| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl2anb | Structured version Visualization version GIF version | ||
| Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |
| Ref | Expression |
|---|---|
| syl2anb.1 | ⊢ (𝜑 ↔ 𝜓) |
| syl2anb.2 | ⊢ (𝜏 ↔ 𝜒) |
| syl2anb.3 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| syl2anb | ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl2anb.2 | . 2 ⊢ (𝜏 ↔ 𝜒) | |
| 2 | syl2anb.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
| 3 | syl2anb.3 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
| 4 | 2, 3 | sylanb 581 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
| 5 | 1, 4 | sylan2b 594 | 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: sylancb 600 rexdifi 4150 reupick3 4330 difprsnss 4799 opthhausdorff 5522 pwssun 5575 trin2 6143 sspred 6330 fundif 6615 fnun 6682 f1cof1 6814 f1oun 6867 f1oco 6871 eqfnfv 7051 eqfunfv 7056 sorpsscmpl 7754 ordsucsssuc 7843 ordsucun 7845 resf1extb 7956 soxp 8154 poseq 8183 ressuppssdif 8210 frrlem4 8314 wfrlem4OLD 8352 issmo 8388 tfrlem5 8420 ener 9041 domtr 9047 unen 9086 xpdom2 9107 mapen 9181 unxpdomlem3 9288 fiin 9462 suc11reg 9659 djuunxp 9961 xpnum 9991 pm54.43 10041 r0weon 10052 fseqen 10067 kmlem9 10199 axpre-lttrn 11206 axpre-mulgt0 11208 wloglei 11795 mulnzcnf 11909 zaddcl 12657 zmulcl 12666 qaddcl 13007 qmulcl 13009 rpaddcl 13057 rpmulcl 13058 rpdivcl 13060 xrltnsym 13179 xrlttri 13181 xmullem 13306 xmulcom 13308 xmulneg1 13311 xmulf 13314 ge0addcl 13500 ge0mulcl 13501 ge0xaddcl 13502 ge0xmulcl 13503 serge0 14097 expclzlem 14124 expge0 14139 expge1 14140 hashfacen 14493 wwlktovf1 14996 nn0rppwr 16598 nn0expgcd 16601 qredeu 16695 nn0gcdsq 16789 mul4sq 16992 fpwipodrs 18585 pwmnd 18950 gimco 19286 gictr 19294 symgextf1 19439 efgrelexlemb 19768 xrs1mnd 21422 pzriprnglem5 21496 pzriprnglem8 21499 lmimco 21864 lmictra 21865 cctop 23013 iscn2 23246 iscnp2 23247 paste 23302 txuni 23600 txcn 23634 txcmpb 23652 tx2ndc 23659 hmphtr 23791 snfil 23872 supfil 23903 filssufilg 23919 tsmsxp 24163 dscmet 24585 rlimcnp 27008 efnnfsumcl 27146 efchtdvds 27202 lgsne0 27379 mul2sq 27463 sltsolem1 27720 ssltsn 27837 nohalf 28407 colinearalglem2 28922 nb3grprlem2 29398 cplgr3v 29452 crctcshwlkn0 29841 wwlksnextinj 29919 hsn0elch 31267 shscli 31336 hsupss 31360 5oalem6 31678 mdsldmd1i 32350 superpos 32373 bnj110 34872 msubco 35536 fnsingle 35920 funimage 35929 funpartfun 35944 mpomulnzcnf 36300 bj-nnfan 36749 bj-nnfor 36751 bj-snsetex 36964 bj-snmoore 37114 difunieq 37375 riscer 37995 divrngidl 38035 dvdsexpnn0 42369 zaddcom 42482 zmulcom 42486 rimco 42528 rictr 42530 mzpincl 42745 kelac2lem 43076 omcl3g 43347 cllem0 43579 unhe1 43798 tz6.12-1-afv 47186 tz6.12-1-afv2 47253 sprsymrelf1 47483 prmdvdsfmtnof1lem2 47572 grictr 47892 usgrexmpl2trifr 47996 uspgrsprf1 48063 2zrngamgm 48161 2zrngmmgm 48168 rrx2xpref1o 48639 f1omo 48792 |
| Copyright terms: Public domain | W3C validator |