Theorem syl2anb 593

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

Ref	Expression
syl2anb.1	⊢ (𝜑 ↔ 𝜓)
syl2anb.2	⊢ (𝜏 ↔ 𝜒)
syl2anb.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anb	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem 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 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

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