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 480 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 481 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏)) |
5 | 2, 4 | bitrd 267 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ 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 196 df-an 385 |
This theorem is referenced by: sylan9bbr 733 bi2anan9 913 baibd 946 rbaibd 947 syl3an9b 1389 nanbi12 1449 sbcom2 2433 2sb5rf 2439 2sb6rf 2440 eqeq12 2623 eleq12 2678 sbhypf 3226 ceqsrex2v 3308 sseq12 3591 2ralsng 4167 rexprg 4182 rextpg 4184 breq12 4588 reusv2lem5 4799 opelopabg 4918 brabg 4919 opelopabgf 4920 opelopab2 4921 rbropapd 4939 ralxpf 5190 feq23 5942 f00 6000 fconstg 6005 f1oeq23 6043 f1o00 6083 fnelfp 6346 fnelnfp 6348 isofrlem 6490 f1oiso 6501 riota1a 6530 cbvmpt2x 6631 caovord 6743 caovord3 6745 f1oweALT 7043 oaordex 7525 oaass 7528 odi 7546 findcard2s 8086 unfilem1 8109 suppeqfsuppbi 8172 oieu 8327 r1pw 8591 carddomi2 8679 isacn 8750 cdadom2 8892 axdc2 9154 alephval2 9273 fpwwe2cbv 9331 fpwwe2lem2 9333 fpwwecbv 9345 fpwwelem 9346 canthwelem 9351 canthwe 9352 distrlem4pr 9727 axpre-sup 9869 nn0ind-raph 11353 xnn0xadd0 11949 elfz 12203 elfzp12 12288 expeq0 12752 leiso 13100 wrd2ind 13329 trcleq12lem 13580 dfrtrclrec2 13645 shftfib 13660 absdvdsb 14838 dvdsabsb 14839 dvdsabseq 14873 unbenlem 15450 isprs 16753 isdrs 16757 pltval 16783 lublecllem 16811 istos 16858 isdlat 17016 znfld 19728 tgss2 20602 isopn2 20646 cnpf2 20864 lmbr 20872 isreg2 20991 fclsrest 21638 qustgplem 21734 ustuqtoplem 21853 xmetec 22049 nmogelb 22330 metdstri 22462 tchcph 22844 ulmval 23938 2lgslem1a 24916 iscgrg 25207 eupath2lem1 26504 eigrei 28077 eigorthi 28080 jplem1 28511 superpos 28597 chrelati 28607 br8d 28802 issiga 29501 eulerpartlemgvv 29765 br8 30899 br6 30900 br4 30901 brsegle 31385 topfne 31519 tailfb 31542 filnetlem1 31543 nndivsub 31626 bj-elequ12 31855 bj-rest10 32222 isbasisrelowllem1 32379 isbasisrelowllem2 32380 wl-2sb6d 32520 curf 32557 curunc 32561 poimirlem26 32605 mblfinlem2 32617 cnambfre 32628 itgaddnclem2 32639 ftc1anclem1 32655 grpokerinj 32862 rngoisoval 32946 smprngopr 33021 ax12eq 33244 ax12el 33245 2llnjN 33871 2lplnj 33924 elpadd0 34113 lauteq 34399 lpolconN 35794 rexrabdioph 36376 eliunov2 36990 nzss 37538 iotasbc2 37643 istrlson 40914 ispthson 40948 isspthson 40949 elwwlks2on 41162 eupth2lem1 41386 cbvmpt2x2 41907 |
Copyright terms: Public domain | W3C validator |