![]() |
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 578 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2b 589 | 1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: sylancb 595 nanassOLD 1638 reupick3 4140 difprsnss 4547 opthhausdorff 5202 pwssun 5245 trin2 5760 sspred 5927 fundif 6170 fnun 6229 fco 6294 f1co 6347 foco 6364 f1oun 6396 f1oco 6399 eqfnfv 6559 eqfunfv 6564 sorpsscmpl 7207 ordsucsssuc 7283 ordsucun 7285 soxp 7553 ressuppssdif 7579 wfrlem4 7682 wfrlem4OLD 7683 issmo 7710 tfrlem5 7741 ener 8268 domtr 8274 unen 8308 xpdom2 8323 mapen 8392 unxpdomlem3 8434 fiin 8596 suc11reg 8792 djuunxp 9059 xpnum 9089 pm54.43 9138 r0weon 9147 fseqen 9162 kmlem9 9294 axpre-lttrn 10302 axpre-mulgt0 10304 wloglei 10883 mulnzcnopr 10997 zaddcl 11744 zmulcl 11753 qaddcl 12086 qmulcl 12088 rpaddcl 12135 rpmulcl 12136 rpdivcl 12138 xrltnsym 12255 xrlttri 12257 xmullem 12381 xmulcom 12383 xmulneg1 12386 xmulf 12389 ge0addcl 12573 ge0mulcl 12574 ge0xaddcl 12575 ge0xmulcl 12576 serge0 13148 expclzlem 13177 expge0 13189 expge1 13190 hashfacen 13526 wwlktovf1 14078 qredeu 15743 nn0gcdsq 15830 mul4sq 16028 fpwipodrs 17516 gimco 18060 gictr 18067 symgextf1 18190 efgrelexlemb 18515 xrs1mnd 20143 lmimco 20549 lmictra 20550 cctop 21180 iscn2 21412 iscnp2 21413 paste 21468 txuni 21765 txcn 21799 txcmpb 21817 tx2ndc 21824 hmphtr 21956 snfil 22037 supfil 22068 filssufilg 22084 tsmsxp 22327 dscmet 22746 rlimcnp 25104 efnnfsumcl 25241 efchtdvds 25297 lgsne0 25472 mul2sq 25556 colinearalglem2 26205 nb3grprlem2 26678 cplgr3v 26732 crctcshwlkn0 27119 wlknwwlksnsurOLD 27189 wlkwwlksurOLD 27197 wwlksnextinj 27212 wwlksnextinjOLD 27217 hsn0elch 28659 shscli 28730 hsupss 28754 5oalem6 29072 mdsldmd1i 29744 superpos 29767 bnj110 31473 msubco 31973 poseq 32291 frrlem4 32321 sltsolem1 32364 fnsingle 32564 funimage 32573 funpartfun 32588 bj-snsetex 33472 bj-snmoore 33590 riscer 34328 divrngidl 34368 mzpincl 38140 kelac2lem 38476 cllem0 38711 unhe1 38918 tz6.12-1-afv 42075 tz6.12-1-afv2 42142 prmdvdsfmtnof1lem2 42326 sprsymrelf1 42592 uspgrsprf1 42601 2zrngamgm 42785 2zrngmmgm 42792 |
Copyright terms: Public domain | W3C validator |