Theorem syl3an3b 1402

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

Ref	Expression
syl3an3b.1	⊢ (𝜑 ↔ 𝜃)
syl3an3b.2	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3an3b	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Proof of Theorem syl3an3b

Step	Hyp	Ref	Expression
1		syl3an3b.1	. . 3 ⊢ (𝜑 ↔ 𝜃)
2	1	biimpi 215	. 2 ⊢ (𝜑 → 𝜃)
3		syl3an3b.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl3an3 1162	1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086

This theorem is referenced by:  fnunres2  6670  fresaunres1  6773  fvun2  6993  fvpr2g  7204  nnmsucr  8650  entrfil  9217  enpr2  10031  xrlttr  13157  iccdil  13505  icccntr  13507  hashgt23el  14421  absexpz  15290  posglbdg  18412  f1omvdco3  19409  isdrngd  20662  isdrngdOLD  20664  unicld  22968  2ndcdisj2  23379  logrec  26713  cdj3lem3  32266  bnj563  34379  bnj1033  34605  lindsadd  37091  nn0rppwr  41896  stoweidlem14  45404

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »