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 484 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
3 | sylan9bb.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
4 | 3 | adantl 485 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏)) |
5 | 2, 4 | bitrd 282 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: sylan9bbr 514 baibd 543 syl3an9b 1436 nanbi12 1499 sbcom2 2167 2sb5rf 2473 2sb6rf 2474 eqeqan12d 2753 eqeq12OLD 2758 eleq12 2829 sbhypf 3482 ceqsrex2v 3580 elabd2 3594 sseq12 3944 csbie2df 4371 2ralsng 4608 rexprgf 4625 rextpg 4631 breq12 5074 reusv2lem5 5311 opelopabg 5435 brabg 5436 opelopabgf 5437 opelopab2 5438 rbropapd 5459 ralxpf 5732 feq23 6550 f00 6622 fconstg 6627 f1oeq23 6673 f1o00 6716 fnelfp 7011 fnelnfp 7013 isofrlem 7170 f1oiso 7181 riota1a 7214 cbvmpox 7325 caovord 7440 caovord3 7442 f1oweALT 7766 oaordex 8309 oaass 8312 odi 8330 findcard2s 8868 unfilem1 8964 suppeqfsuppbi 9028 oieu 9184 r1pw 9490 carddomi2 9615 isacn 9687 djudom2 9826 axdc2 10092 alephval2 10215 fpwwe2cbv 10273 fpwwe2lem2 10275 fpwwecbv 10287 fpwwelem 10288 canthwelem 10293 canthwe 10294 distrlem4pr 10669 axpre-sup 10812 nn0ind-raph 12306 elpq 12600 xnn0xadd0 12866 elfz 13130 elfzp12 13220 expeq0 13697 leiso 14057 wrd2ind 14320 trcleq12lem 14588 dfrtrclrec2 14653 shftfib 14667 absdvdsb 15868 dvdsabsb 15869 dvdsabseq 15906 unbenlem 16493 isprs 17836 isdrs 17840 pltval 17870 lublecllem 17898 istos 17956 isdlat 18060 znfld 20557 tgss2 21915 isopn2 21960 cnpf2 22178 lmbr 22186 isreg2 22305 fclsrest 22952 qustgplem 23049 ustuqtoplem 23168 xmetec 23363 nmogelb 23645 metdstri 23779 tcphcph 24165 ulmval 25303 2lgslem1a 26303 iscgrg 26634 istrlson 27825 ispthson 27860 isspthson 27861 elwwlks2on 28074 eupth2lem1 28332 eigrei 29946 eigorthi 29949 jplem1 30380 superpos 30466 chrelati 30476 br8d 30700 issiga 31823 eulerpartlemgvv 32086 cplgredgex 32825 acycgrcycl 32852 br8 33472 br6 33473 br4 33474 elmade 33821 brsegle 34180 topfne 34313 tailfb 34336 filnetlem1 34337 nndivsub 34416 bj-elequ12 34630 bj-rest10 35029 isbasisrelowllem1 35299 isbasisrelowllem2 35300 fvineqsnf1 35354 wl-2sb6d 35486 curf 35528 curunc 35532 poimirlem26 35576 mblfinlem2 35588 cnambfre 35598 itgaddnclem2 35609 ftc1anclem1 35623 grpokerinj 35824 rngoisoval 35908 smprngopr 35983 ax12eq 36728 ax12el 36729 2llnjN 37354 2lplnj 37407 elpadd0 37596 lauteq 37882 lpolconN 39274 rexrabdioph 40366 eliunov2 41011 nzss 41655 iotasbc2 41758 or2expropbilem2 44244 elsetpreimafvbi 44561 reuopreuprim 44696 cbvmpox2 45389 naryfvalel 45694 line2x 45818 |
Copyright terms: Public domain | W3C validator |