![]() |
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 579 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2b 592 | 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: sylancb 598 rexdifi 4146 reupick3 4323 difprsnss 4807 opthhausdorff 5523 pwssun 5577 trin2 6134 sspred 6319 fundif 6607 fnun 6673 fcoOLD 6753 f1cof1 6809 f1coOLD 6811 f1oun 6863 f1oco 6867 eqfnfv 7045 eqfunfv 7050 sorpsscmpl 7745 ordsucsssuc 7832 ordsucun 7834 soxp 8140 poseq 8169 ressuppssdif 8196 frrlem4 8301 wfrlem4OLD 8339 issmo 8375 tfrlem5 8407 ener 9028 domtr 9034 unen 9077 xpdom2 9098 mapen 9172 unxpdomlem3 9283 fiin 9453 suc11reg 9650 djuunxp 9952 xpnum 9982 pm54.43 10032 r0weon 10043 fseqen 10058 kmlem9 10189 axpre-lttrn 11197 axpre-mulgt0 11199 wloglei 11784 mulnzcnf 11898 zaddcl 12640 zmulcl 12649 qaddcl 12987 qmulcl 12989 rpaddcl 13036 rpmulcl 13037 rpdivcl 13039 xrltnsym 13156 xrlttri 13158 xmullem 13283 xmulcom 13285 xmulneg1 13288 xmulf 13291 ge0addcl 13477 ge0mulcl 13478 ge0xaddcl 13479 ge0xmulcl 13480 serge0 14061 expclzlem 14088 expge0 14103 expge1 14104 hashfacen 14453 hashfacenOLD 14454 wwlktovf1 14948 qredeu 16636 nn0gcdsq 16731 mul4sq 16930 fpwipodrs 18539 pwmnd 18896 gimco 19229 gictr 19237 symgextf1 19383 efgrelexlemb 19712 xrs1mnd 21344 pzriprnglem5 21418 pzriprnglem8 21421 lmimco 21785 lmictra 21786 cctop 22929 iscn2 23162 iscnp2 23163 paste 23218 txuni 23516 txcn 23550 txcmpb 23568 tx2ndc 23575 hmphtr 23707 snfil 23788 supfil 23819 filssufilg 23835 tsmsxp 24079 dscmet 24501 rlimcnp 26917 efnnfsumcl 27055 efchtdvds 27111 lgsne0 27288 mul2sq 27372 sltsolem1 27628 ssltsn 27745 colinearalglem2 28738 nb3grprlem2 29214 cplgr3v 29268 crctcshwlkn0 29652 wwlksnextinj 29730 hsn0elch 31078 shscli 31147 hsupss 31171 5oalem6 31489 mdsldmd1i 32161 superpos 32184 bnj110 34522 msubco 35174 fnsingle 35548 funimage 35557 funpartfun 35572 mpomulnzcnf 35816 bj-nnfan 36258 bj-nnfor 36260 bj-snsetex 36475 bj-snmoore 36625 difunieq 36886 riscer 37494 divrngidl 37534 rimco 41786 rictr 41788 nn0rppwr 41924 nn0expgcd 41926 dvdsexpnn0 41932 zaddcom 42038 zmulcom 42042 mzpincl 42185 kelac2lem 42519 omcl3g 42794 cllem0 43027 unhe1 43246 tz6.12-1-afv 46583 tz6.12-1-afv2 46650 sprsymrelf1 46865 prmdvdsfmtnof1lem2 46954 grictr 47267 uspgrsprf1 47287 2zrngamgm 47385 2zrngmmgm 47392 rrx2xpref1o 47869 f1omo 47991 |
Copyright terms: Public domain | W3C validator |