![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9bbr | Structured version Visualization version GIF version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
Ref | Expression |
---|---|
sylan9bbr.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
sylan9bbr.2 | ⊢ (𝜃 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
sylan9bbr | ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9bbr.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | sylan9bbr.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
3 | 1, 2 | sylan9bb 736 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
4 | 3 | ancoms 468 | 1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: pm5.75 998 sbcom2 2473 sbal1 2488 sbal2 2489 mpteq12f 4764 otthg 4983 fmptsng 6475 f1oiso 6641 mpt2eq123 6756 elovmpt2rab 6922 elovmpt2rab1 6923 ovmpt3rabdm 6934 elovmpt3rab1 6935 tfindsg 7102 findsg 7135 dfoprab4f 7270 opiota 7273 fmpt2x 7281 oalimcl 7685 oeeui 7727 nnmword 7758 isinf 8214 elfi 8360 brwdomn0 8515 alephval3 8971 dfac2 8991 fin17 9254 isfin7-2 9256 ltmpi 9764 addclprlem1 9876 distrlem4pr 9886 1idpr 9889 qreccl 11846 0fz1 12399 zmodid2 12738 ccatrcl1 13412 eqwrds3 13750 divgcdcoprm0 15426 sscntz 17805 gexdvds 18045 cnprest 21141 txrest 21482 ptrescn 21490 flimrest 21834 txflf 21857 fclsrest 21875 tsmssubm 21993 mbfi1fseqlem4 23530 axcontlem7 25895 uhgreq12g 26005 nbuhgr2vtx1edgb 26293 wlkcomp 26582 uhgrwkspthlem2 26706 clwlkcomp 26731 hashecclwwlkn1 27041 umgrhashecclwwlk 27042 numclwlk1lem2fo 27348 ubthlem1 27854 pjimai 29163 atcv1 29367 chirredi 29381 bj-restsn 33160 wl-sbcom2d-lem1 33472 wl-sbalnae 33475 ptrest 33538 poimirlem28 33567 heicant 33574 ftc1anclem1 33615 sbeqi 34098 ralbi12f 34099 iineq12f 34103 brcnvepres 34174 nzss 38833 raaan2 41496 rngcinv 42306 rngcinvALTV 42318 ringcinv 42357 ringcinvALTV 42381 snlindsntorlem 42584 |
Copyright terms: Public domain | W3C validator |