![]() |
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 474 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 475 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏)) |
5 | 2, 4 | bitrd 271 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: sylan9bbr 506 baibd 535 rbaibd 536 bi2anan9 629 syl3an9b 1507 nanbi12 1573 sbcom2 2523 sbcom2OLD 2524 2sb5rf 2530 2sb6rf 2531 2sb6rfOLD 2532 eqeq12 2791 eleq12 2849 sbhypf 3455 ceqsrex2v 3541 sseq12 3847 2ralsng 4447 rexprgf 4462 rextpg 4466 breq12 4893 reusv2lem5 5116 opelopabg 5232 brabg 5233 opelopabgf 5234 opelopab2 5235 rbropapd 5254 ralxpf 5516 feq23 6277 f00 6339 fconstg 6344 f1oeq23 6385 f1o00 6427 fnelfp 6710 fnelnfp 6712 isofrlem 6864 f1oiso 6875 riota1a 6904 cbvmpt2x 7012 caovord 7124 caovord3 7126 f1oweALT 7431 oaordex 7924 oaass 7927 odi 7945 findcard2s 8491 unfilem1 8514 suppeqfsuppbi 8579 oieu 8735 r1pw 9007 carddomi2 9131 isacn 9202 cdadom2 9346 axdc2 9608 alephval2 9731 fpwwe2cbv 9789 fpwwe2lem2 9791 fpwwecbv 9803 fpwwelem 9804 canthwelem 9809 canthwe 9810 distrlem4pr 10185 axpre-sup 10328 nn0ind-raph 11833 elpq 12126 xnn0xadd0 12393 elfz 12653 elfzp12 12741 expeq0 13212 leiso 13561 wrd2ind 13848 wrd2indOLD 13849 trcleq12lem 14145 dfrtrclrec2 14208 shftfib 14223 absdvdsb 15411 dvdsabsb 15412 dvdsabseq 15446 unbenlem 16020 isprs 17320 isdrs 17324 pltval 17350 lublecllem 17378 istos 17425 isdlat 17583 znfld 20308 tgss2 21203 isopn2 21248 cnpf2 21466 lmbr 21474 isreg2 21593 fclsrest 22240 qustgplem 22336 ustuqtoplem 22455 xmetec 22651 nmogelb 22932 metdstri 23066 tcphcph 23447 ulmval 24575 2lgslem1a 25572 iscgrg 25867 istrlson 27063 ispthson 27098 isspthson 27099 elwwlks2on 27343 eupth2lem1 27626 eigrei 29269 eigorthi 29272 jplem1 29703 superpos 29789 chrelati 29799 vtocl2d 29890 br8d 29989 issiga 30776 eulerpartlemgvv 31040 br8 32244 br6 32245 br4 32246 brsegle 32808 topfne 32941 tailfb 32964 filnetlem1 32965 nndivsub 33043 bj-elequ12 33261 bj-rest10 33618 isbasisrelowllem1 33801 isbasisrelowllem2 33802 wl-2sb6d 33938 curf 34017 curunc 34021 poimirlem26 34066 mblfinlem2 34078 cnambfre 34088 itgaddnclem2 34099 ftc1anclem1 34115 grpokerinj 34321 rngoisoval 34405 smprngopr 34480 ax12eq 35100 ax12el 35101 2llnjN 35726 2lplnj 35779 elpadd0 35968 lauteq 36254 lpolconN 37646 rexrabdioph 38328 eliunov2 38938 nzss 39482 iotasbc2 39586 cbvmpt2x2 43139 line2x 43500 |
Copyright terms: Public domain | W3C validator |