![]() |
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 2470 2sb6rf 2471 eqeqan12d 2750 eqeq12OLD 2755 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 7332 cbvmpox 7446 caovord 7561 caovord3 7563 f1oweALT 7901 oaordex 8501 oaass 8504 odi 8522 findcard2s 9105 unfilem1 9250 suppeqfsuppbi 9315 oieu 9471 r1pw 9777 carddomi2 9902 isacn 9976 djudom2 10115 axdc2 10381 alephval2 10504 fpwwe2cbv 10562 fpwwe2lem2 10564 fpwwecbv 10576 fpwwelem 10577 canthwelem 10582 canthwe 10583 distrlem4pr 10958 axpre-sup 11101 nn0ind-raph 12599 elpq 12892 xnn0xadd0 13158 elfz 13422 elfzp12 13512 expeq0 13990 leiso 14350 wrd2ind 14603 trcleq12lem 14870 dfrtrclrec2 14935 shftfib 14949 absdvdsb 16149 dvdsabsb 16150 dvdsabseq 16187 unbenlem 16772 isprs 18178 isdrs 18182 pltval 18213 lublecllem 18241 istos 18299 isdlat 18403 znfld 20952 tgss2 22321 isopn2 22367 cnpf2 22585 lmbr 22593 isreg2 22712 fclsrest 23359 qustgplem 23456 ustuqtoplem 23575 xmetec 23771 nmogelb 24064 metdstri 24198 tcphcph 24585 ulmval 25723 2lgslem1a 26723 elmade 27181 iscgrg 27340 istrlson 28541 ispthson 28576 isspthson 28577 elwwlks2on 28790 eupth2lem1 29048 eigrei 30662 eigorthi 30665 jplem1 31096 superpos 31182 chrelati 31192 br8d 31415 issiga 32580 eulerpartlemgvv 32845 cplgredgex 33583 acycgrcycl 33610 br8 34199 br6 34200 br4 34201 brsegle 34660 topfne 34793 tailfb 34816 filnetlem1 34817 nndivsub 34896 bj-elequ12 35110 bj-rest10 35526 isbasisrelowllem1 35793 isbasisrelowllem2 35794 fvineqsnf1 35848 wl-2sb6d 35980 curf 36023 curunc 36027 poimirlem26 36071 mblfinlem2 36083 cnambfre 36093 itgaddnclem2 36104 ftc1anclem1 36118 grpokerinj 36319 rngoisoval 36403 smprngopr 36478 parteq12 37205 ax12eq 37370 ax12el 37371 2llnjN 37997 2lplnj 38050 elpadd0 38239 lauteq 38525 lpolconN 39917 rexrabdioph 41055 eliunov2 41893 nzss 42539 iotasbc2 42642 or2expropbilem2 45199 elsetpreimafvbi 45515 reuopreuprim 45650 cbvmpox2 46343 naryfvalel 46648 line2x 46772 |
Copyright terms: Public domain | W3C validator |