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 584 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | sylan2b 597 | 1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: sylancb 603 rexdifi 4074 reupick3 4248 difprsnss 4726 opthhausdorff 5414 pwssun 5465 trin2 6002 sspred 6183 fundif 6446 fnun 6508 fcoOLD 6588 f1cof1 6644 f1coOLD 6646 f1oun 6698 f1oco 6701 eqfnfv 6870 eqfunfv 6875 sorpsscmpl 7540 ordsucsssuc 7620 ordsucun 7622 soxp 7916 ressuppssdif 7947 frrlem4 8050 wfrlem4 8078 issmo 8105 tfrlem5 8136 ener 8697 domtr 8703 unen 8745 xpdom2 8762 mapen 8832 unxpdomlem3 8908 fiin 9062 suc11reg 9258 djuunxp 9561 xpnum 9591 pm54.43 9641 r0weon 9650 fseqen 9665 kmlem9 9796 axpre-lttrn 10804 axpre-mulgt0 10806 wloglei 11388 mulnzcnopr 11502 zaddcl 12241 zmulcl 12250 qaddcl 12585 qmulcl 12587 rpaddcl 12632 rpmulcl 12633 rpdivcl 12635 xrltnsym 12751 xrlttri 12753 xmullem 12878 xmulcom 12880 xmulneg1 12883 xmulf 12886 ge0addcl 13072 ge0mulcl 13073 ge0xaddcl 13074 ge0xmulcl 13075 serge0 13654 expclzlem 13683 expge0 13695 expge1 13696 hashfacen 14042 hashfacenOLD 14043 wwlktovf1 14548 qredeu 16239 nn0gcdsq 16332 mul4sq 16531 fpwipodrs 18070 pwmnd 18388 gimco 18696 gictr 18703 symgextf1 18837 efgrelexlemb 19164 xrs1mnd 20425 lmimco 20830 lmictra 20831 cctop 21927 iscn2 22159 iscnp2 22160 paste 22215 txuni 22513 txcn 22547 txcmpb 22565 tx2ndc 22572 hmphtr 22704 snfil 22785 supfil 22816 filssufilg 22832 tsmsxp 23076 dscmet 23494 rlimcnp 25872 efnnfsumcl 26009 efchtdvds 26065 lgsne0 26240 mul2sq 26324 colinearalglem2 27022 nb3grprlem2 27493 cplgr3v 27547 crctcshwlkn0 27929 wwlksnextinj 28007 hsn0elch 29353 shscli 29422 hsupss 29446 5oalem6 29764 mdsldmd1i 30436 superpos 30459 bnj110 32574 msubco 33229 poseq 33565 sltsolem1 33641 fnsingle 33984 funimage 33993 funpartfun 34008 bj-nnfan 34693 bj-nnfor 34695 bj-snsetex 34916 bj-snmoore 35045 difunieq 35308 riscer 35909 divrngidl 35949 nn0rppwr 40069 nn0expgcd 40071 dvdsexpnn0 40077 mzpincl 40287 kelac2lem 40620 cllem0 40877 unhe1 41098 tz6.12-1-afv 44366 tz6.12-1-afv2 44433 sprsymrelf1 44649 prmdvdsfmtnof1lem2 44738 uspgrsprf1 45010 2zrngamgm 45198 2zrngmmgm 45205 rrx2xpref1o 45765 f1omo 45889 |
Copyright terms: Public domain | W3C validator |