![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9bbr | Structured version Visualization version GIF version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
Ref | Expression |
---|---|
sylan9bbr.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
sylan9bbr.2 | ⊢ (𝜃 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
sylan9bbr | ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9bbr.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | sylan9bbr.2 | . . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏)) | |
3 | 1, 2 | sylan9bb 508 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) |
4 | 3 | ancoms 457 | 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: bimsc1 842 pm5.75 1026 sbcom2 2162 sbal1 2521 sbal2 2522 raaan2 4526 mpteq12f 5237 otthg 5487 fmptsng 7177 f1oiso 7358 mpoeq123 7492 elovmporab 7667 elovmporab1w 7668 elovmporab1 7669 ovmpt3rabdm 7680 elovmpt3rab1 7681 tfindsg 7866 findsg 7905 dfoprab4f 8061 opiota 8064 fmpox 8072 oalimcl 8581 oeeui 8623 nnmword 8654 isinf 9285 isinfOLD 9286 elfi 9438 brwdomn0 9594 alephval3 10135 dfac2b 10155 fin17 10419 isfin7-2 10421 ltmpi 10929 addclprlem1 11041 distrlem4pr 11051 1idpr 11054 qreccl 12986 0fz1 13556 zmodid2 13900 ccatrcl1 14580 eqwrds3 14948 divgcdcoprm0 16639 sscntz 19289 gexdvds 19551 rngcinv 20582 cnprest 23237 txrest 23579 ptrescn 23587 flimrest 23931 txflf 23954 fclsrest 23972 tsmssubm 24091 mbfi1fseqlem4 25692 2sq2 27411 axcontlem7 28853 uhgreq12g 28950 nbuhgr2vtx1edgb 29237 wlkcomp 29517 uhgrwkspthlem2 29640 clwlkcomp 29665 wlknwwlksnbij 29771 hashecclwwlkn1 29959 umgrhashecclwwlk 29960 numclwwlk1lem2fo 30240 ubthlem1 30752 pjimai 32058 atcv1 32262 chirredi 32276 bj-restsn 36689 fvineqsneu 37018 pibt2 37024 wl-sbcom2d-lem1 37154 wl-sbalnae 37157 ptrest 37220 poimirlem28 37249 heicant 37256 ftc1anclem1 37294 sbeqi 37760 ralbi12f 37761 iineq12f 37765 brcnvepres 37866 elrnressn 37872 tfsconcat0i 42913 nzss 43893 or2expropbilem1 46549 ich2exprop 46945 ichnreuop 46946 ichreuopeq 46947 reuopreuprim 47000 rngcinvALTV 47521 snlindsntorlem 47721 itscnhlc0xyqsol 48021 opndisj 48104 |
Copyright terms: Public domain | W3C validator |