![]() |
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 479 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 480 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏)) |
5 | 2, 4 | bitrd 278 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 |
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 395 |
This theorem is referenced by: sylan9bbr 509 baibd 538 syl3an9b 1430 nanbi12 1496 sbcom2 2162 2sb5rf 2465 2sb6rf 2466 eqeqan12d 2739 eqeq12OLD 2744 eleq12 2815 sbhypfOLD 3529 ceqsrex2v 3641 elabd2 3655 sseq12 4004 csbie2df 4442 2ralsng 4682 rexprgf 4699 rextpg 4705 breq12 5154 reusv2lem5 5402 opelopabg 5540 brabg 5541 opelopabgf 5542 opelopab2 5543 rbropapd 5566 ralxpf 5849 feq23 6707 f00 6779 fconstg 6784 f1oeq23 6829 f1o00 6873 fnelfp 7184 fnelnfp 7186 isofrlem 7347 f1oiso 7358 riota1a 7398 cbvmpox 7513 caovord 7632 caovord3 7634 f1oweALT 7977 oaordex 8579 oaass 8582 odi 8600 findcard2s 9190 unfilem1 9335 suppeqfsuppbi 9404 oieu 9564 r1pw 9870 carddomi2 9995 isacn 10069 djudom2 10208 axdc2 10474 alephval2 10597 fpwwe2cbv 10655 fpwwe2lem2 10657 fpwwecbv 10669 fpwwelem 10670 canthwelem 10675 canthwe 10676 distrlem4pr 11051 axpre-sup 11194 nn0ind-raph 12695 elpq 12992 xnn0xadd0 13261 elfz 13525 elfzp12 13615 expeq0 14093 leiso 14456 wrd2ind 14709 trcleq12lem 14976 dfrtrclrec2 15041 shftfib 15055 absdvdsb 16255 dvdsabsb 16256 dvdsabseq 16293 unbenlem 16880 isprs 18292 isdrs 18296 pltval 18327 lublecllem 18355 istos 18413 isdlat 18517 znfld 21511 tgss2 22934 isopn2 22980 cnpf2 23198 lmbr 23206 isreg2 23325 fclsrest 23972 qustgplem 24069 ustuqtoplem 24188 xmetec 24384 nmogelb 24677 metdstri 24811 tcphcph 25209 ulmval 26361 2lgslem1a 27369 elmade 27840 iscgrg 28388 istrlson 29593 ispthson 29628 isspthson 29629 elwwlks2on 29842 eupth2lem1 30100 eigrei 31716 eigorthi 31719 jplem1 32150 superpos 32236 chrelati 32246 br8d 32479 ellpi 33185 issiga 33862 eulerpartlemgvv 34127 cplgredgex 34861 acycgrcycl 34888 br8 35481 br6 35482 br4 35483 brsegle 35835 topfne 35969 tailfb 35992 filnetlem1 35993 nndivsub 36072 bj-elequ12 36286 bj-rest10 36698 isbasisrelowllem1 36965 isbasisrelowllem2 36966 fvineqsnf1 37020 wl-2sb6d 37156 curf 37202 curunc 37206 poimirlem26 37250 mblfinlem2 37262 cnambfre 37272 itgaddnclem2 37283 ftc1anclem1 37297 grpokerinj 37497 rngoisoval 37581 smprngopr 37656 parteq12 38378 ax12eq 38543 ax12el 38544 2llnjN 39170 2lplnj 39223 elpadd0 39412 lauteq 39698 lpolconN 41090 f1o2d2 41857 rexrabdioph 42356 tfsnfin 42923 eliunov2 43251 nzss 43896 iotasbc2 43999 or2expropbilem2 46553 elsetpreimafvbi 46868 reuopreuprim 47003 cbvmpox2 47585 naryfvalel 47889 line2x 48013 |
Copyright terms: Public domain | W3C validator |