|   | 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 279 | 1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: sylan9bbr 510 baibd 539 syl3an9b 1435 nanbi12 1502 elequ12 2125 sbcom2 2172 2sb5rf 2476 2sb6rf 2477 eqeqan12d 2750 eqeq12OLD 2755 eleq12 2830 sbhypfOLD 3544 ceqsrex2v 3657 elabd2 3669 sseq12 4010 csbie2df 4442 2ralsng 4677 rexprgf 4694 rextpg 4698 breq12 5147 reusv2lem5 5401 opelopabg 5542 brabg 5543 opelopabgf 5544 opelopab2 5545 rbropapd 5568 poeq12d 5596 soeq12d 5614 freq12d 5653 seeq12d 5656 weeq12d 5673 ralxpf 5856 feq23 6718 f00 6789 fconstg 6794 f1oeq23 6838 f1o00 6882 fnelfp 7196 fnelnfp 7198 isofrlem 7361 f1oiso 7372 riota1a 7411 cbvmpox 7527 caovord 7645 caovord3 7647 f1oweALT 7998 oaordex 8597 oaass 8600 odi 8618 findcard2s 9206 unfilem1 9344 suppeqfsuppbi 9420 oieu 9580 r1pw 9886 carddomi2 10011 isacn 10085 djudom2 10225 axdc2 10490 alephval2 10613 distrlem4pr 11067 axpre-sup 11210 nn0ind-raph 12720 elpq 13018 xnn0xadd0 13290 elfz 13554 elfzp12 13644 expeq0 14134 leiso 14499 wrd2ind 14762 trcleq12lem 15033 dfrtrclrec2 15098 shftfib 15112 absdvdsb 16313 dvdsabsb 16314 dvdsabseq 16351 unbenlem 16947 isprs 18343 isdrs 18348 pltval 18378 lublecllem 18406 istos 18464 isdlat 18568 znfld 21580 tgss2 22995 isopn2 23041 cnpf2 23259 lmbr 23267 isreg2 23386 fclsrest 24033 qustgplem 24130 ustuqtoplem 24249 xmetec 24445 nmogelb 24738 metdstri 24874 tcphcph 25272 ulmval 26424 2lgslem1a 27436 elmade 27907 iscgrg 28521 istrlson 29726 ispthson 29763 isspthson 29764 elwwlks2on 29980 eupth2lem1 30238 eigrei 31854 eigorthi 31857 jplem1 32288 superpos 32374 chrelati 32384 bian1d 32476 br8d 32623 ellpi 33402 issiga 34114 eulerpartlemgvv 34379 cplgredgex 35127 acycgrcycl 35153 br8 35757 br6 35758 br4 35759 brsegle 36110 topfne 36356 tailfb 36379 filnetlem1 36380 nndivsub 36459 bj-rest10 37090 isbasisrelowllem1 37357 isbasisrelowllem2 37358 fvineqsnf1 37412 wl-2sb6d 37560 curf 37606 curunc 37610 poimirlem26 37654 mblfinlem2 37666 cnambfre 37676 itgaddnclem2 37687 ftc1anclem1 37701 grpokerinj 37901 rngoisoval 37985 smprngopr 38060 parteq12 38778 ax12eq 38943 ax12el 38944 2llnjN 39570 2lplnj 39623 elpadd0 39812 lauteq 40098 lpolconN 41490 f1o2d2 42274 rexrabdioph 42810 tfsnfin 43370 eliunov2 43697 nzss 44341 iotasbc2 44444 or2expropbilem2 47050 elsetpreimafvbi 47383 reuopreuprim 47518 grlicref 47977 cbvmpox2 48257 naryfvalel 48556 line2x 48680 brab2ddw 48747 brab2ddw2 48748 | 
| Copyright terms: Public domain | W3C validator |