|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > syl3an3b | Structured version Visualization version GIF version | ||
| Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) | 
| Ref | Expression | 
|---|---|
| syl3an3b.1 | ⊢ (𝜑 ↔ 𝜃) | 
| syl3an3b.2 | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | 
| Ref | Expression | 
|---|---|
| syl3an3b | ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | syl3an3b.1 | . . 3 ⊢ (𝜑 ↔ 𝜃) | |
| 2 | 1 | biimpi 216 | . 2 ⊢ (𝜑 → 𝜃) | 
| 3 | syl3an3b.2 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) | |
| 4 | 2, 3 | syl3an3 1165 | 1 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ w3a 1086 | 
| 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 207 df-an 396 df-3an 1088 | 
| This theorem is referenced by: fnunres2 6680 fresaunres1 6780 fvun2 7000 fvpr2g 7212 nnmsucr 8664 entrfil 9226 enpr2 10043 xrlttr 13183 iccdil 13531 icccntr 13533 hashgt23el 14464 absexpz 15345 nn0rppwr 16599 posglbdg 18461 f1omvdco3 19468 isdrngd 20766 isdrngdOLD 20768 unicld 23055 2ndcdisj2 23466 logrec 26807 cdj3lem3 32458 bnj563 34758 bnj1033 34984 lindsadd 37621 stoweidlem14 46034 | 
| Copyright terms: Public domain | W3C validator |