![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9bb | Structured version Visualization version GIF version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
Ref | Expression |
---|---|
sylan9bb.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
sylan9bb.2 | ⊢ (𝜃 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
sylan9bb | ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9bb.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | adantr 481 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 482 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏)) |
5 | 2, 4 | bitrd 278 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 |
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 397 |
This theorem is referenced by: sylan9bbr 511 baibd 540 syl3an9b 1434 nanbi12 1501 sbcom2 2161 2sb5rf 2471 2sb6rf 2472 eqeqan12d 2751 eqeq12OLD 2756 eleq12 2827 sbhypfOLD 3506 ceqsrex2v 3606 elabd2 3620 sseq12 3969 csbie2df 4398 2ralsng 4635 rexprgf 4652 rextpg 4658 breq12 5108 reusv2lem5 5355 opelopabg 5493 brabg 5494 opelopabgf 5495 opelopab2 5496 rbropapd 5519 ralxpf 5800 feq23 6649 f00 6721 fconstg 6726 f1oeq23 6772 f1o00 6816 fnelfp 7117 fnelnfp 7119 isofrlem 7281 f1oiso 7292 riota1a 7330 cbvmpox 7444 caovord 7559 caovord3 7561 f1oweALT 7897 oaordex 8497 oaass 8500 odi 8518 findcard2s 9067 unfilem1 9212 suppeqfsuppbi 9277 oieu 9433 r1pw 9739 carddomi2 9864 isacn 9938 djudom2 10077 axdc2 10343 alephval2 10466 fpwwe2cbv 10524 fpwwe2lem2 10526 fpwwecbv 10538 fpwwelem 10539 canthwelem 10544 canthwe 10545 distrlem4pr 10920 axpre-sup 11063 nn0ind-raph 12561 elpq 12854 xnn0xadd0 13120 elfz 13384 elfzp12 13474 expeq0 13952 leiso 14312 wrd2ind 14569 trcleq12lem 14838 dfrtrclrec2 14903 shftfib 14917 absdvdsb 16117 dvdsabsb 16118 dvdsabseq 16155 unbenlem 16740 isprs 18146 isdrs 18150 pltval 18181 lublecllem 18209 istos 18267 isdlat 18371 znfld 20920 tgss2 22289 isopn2 22335 cnpf2 22553 lmbr 22561 isreg2 22680 fclsrest 23327 qustgplem 23424 ustuqtoplem 23543 xmetec 23739 nmogelb 24032 metdstri 24166 tcphcph 24553 ulmval 25691 2lgslem1a 26691 elmade 27149 iscgrg 27283 istrlson 28484 ispthson 28519 isspthson 28520 elwwlks2on 28733 eupth2lem1 28991 eigrei 30605 eigorthi 30608 jplem1 31039 superpos 31125 chrelati 31135 br8d 31358 issiga 32523 eulerpartlemgvv 32788 cplgredgex 33526 acycgrcycl 33553 br8 34145 br6 34146 br4 34147 brsegle 34631 topfne 34764 tailfb 34787 filnetlem1 34788 nndivsub 34867 bj-elequ12 35081 bj-rest10 35497 isbasisrelowllem1 35764 isbasisrelowllem2 35765 fvineqsnf1 35819 wl-2sb6d 35951 curf 35994 curunc 35998 poimirlem26 36042 mblfinlem2 36054 cnambfre 36064 itgaddnclem2 36075 ftc1anclem1 36089 grpokerinj 36290 rngoisoval 36374 smprngopr 36449 parteq12 37176 ax12eq 37341 ax12el 37342 2llnjN 37968 2lplnj 38021 elpadd0 38210 lauteq 38496 lpolconN 39888 rexrabdioph 41026 eliunov2 41862 nzss 42508 iotasbc2 42611 or2expropbilem2 45168 elsetpreimafvbi 45484 reuopreuprim 45619 cbvmpox2 46312 naryfvalel 46617 line2x 46741 |
Copyright terms: Public domain | W3C validator |