Theorem sylan2 270

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
sylan2.1	⊢ (φ → χ)
sylan2.2	⊢ ((ψ ∧ χ) → θ)

Assertion

Ref	Expression
sylan2	⊢ ((ψ ∧ φ) → θ)

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan2.1	. . 3 ⊢ (φ → χ)
2	1	adantl 262	. 2 ⊢ ((ψ ∧ φ) → χ)
3		sylan2.2	. 2 ⊢ ((ψ ∧ χ) → θ)
4	2, 3	syldan 266	1 ⊢ ((ψ ∧ φ) → θ)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  sylan2b  271  sylan2br  272  syl2an  273  sylanr1  384  sylanr2  385  mpanr2  414  adantrl  447  adantrr  448  ancom2s  500  3adantr1  1062  3adantr2  1063  3adantr3  1064  syl3anr1  1186  syl3anr3  1188  dfbi3dc  1285  xordidc  1287  elabgt  2678  sbciegft  2787  csbtt  2856  csbnestgf  2892  copsex2t  3973  pofun  4040  onsucmin  4198  onsucelsucr  4199  onsucsssucr  4200  ordsucunielexmid  4216  ordsuc  4241  nlimsucg  4242  elnn  4271  xpsspw  4393  elxp4  4751  elxp5  4752  funimass2  4920  imain  4924  funimaexg  4926  dff1o2  5074  resdif  5091  funbrfv  5155  fvelimab  5172  eqfnfv2  5209  fvimacnvi  5224  ffvresb  5271  fnressn  5292  fmptapd  5297  fnex  5326  rexima  5337  ralima  5338  f1elima  5355  fnotovb  5490  mpt2eq12  5507  fovrn  5585  fnovrn  5590  ofrfval  5662  fnofval  5663  cofunexg  5680  cofunex2g  5681  mpt2exxg  5775  mpt2exg  5776  f1o2ndf1  5791  smodm2  5851  tfrlem9  5876  tfrlemibxssdm  5882  tfri3  5894  rdgtfr  5901  rdgruledefgg  5902  frecsuclem1  5926  oav2  5982  oasuc  5983  omv2  5984  onasuc  5985  omsuc  5990  onmsuc  5991  nnaass  6003  nndi  6004  nndir  6008  nnaword  6020  ecelqsg  6095  iinerm  6114  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  domentr  6207  xpdom1g  6243  fopwdom  6246  ssfiexmid  6254  addclpi  6311  addasspig  6314  mulasspig  6316  distrpig  6317  mulcanpig  6319  nnppipi  6327  enqdc1  6346  addassnqg  6366  ltbtwnnqq  6398  prarloclemarch  6401  prarloclemarch2  6402  enq0sym  6415  enq0ref  6416  addclnq0  6434  nqpnq0nq  6436  nnanq0  6441  distrnq0  6442  addassnq0lemcl  6444  addassnq0  6445  distnq0r  6446  prarloclemlt  6476  genpassl  6507  genpassu  6508  genpassg  6509  addcomprg  6554  mulcomprg  6556  distrlem1prl  6558  distrlem1pru  6559  1idprl  6566  1idpru  6567  recexprlemdisj  6602  recexprlem1ssl  6605  ax1rid  6761  le2tri3i  6923  add4  6969  cnegexlem1  6983  cnegexlem3  6985  cnegex  6986  subadd  7011  addsub  7019  addsubeq4  7023  negdi  7064  renegcl  7068  resubcl  7071  subdi  7178  mulneg2  7189  mul2neg  7191  submul2  7192  ltnegcon2  7254  lenegcon2  7257  lesub0  7269  cru  7386  recextlem1  7414  recexap  7416  div12ap  7455  divnegap  7465  letrp1  7595  peano2nn  7707  nndivre  7730  nnsub  7733  nndivtr  7736  arch  7954  bndndx  7956  nn0addge1  8004  nn0addge2  8005  zaddcl  8061  zsubcl  8062  zltnle  8067  zrevaddcl  8071  zleltp1  8075  zltlem1  8077  zdiv  8104  peano2uz2  8121  uzind  8125  eluzp1l  8273  ublbneg  8324  qaddcl  8346  qsubcl  8349  qreccl  8351  qdivcl  8352  qrevaddcl  8353  irradd  8355  irrmul  8356  rerpdivcl  8388  xrre  8503  elioc2  8575  icoshft  8628  iccdil  8636  fzss2  8697  fzsuc2  8711  fzrev2  8717  elfzm11  8723  elfzp1b  8729  fzrevral  8737  fzshftral  8740  fzof  8771  fzoval  8775  fzon  8792  fzosubel  8820  zpnn0elfzo  8833  elfzom1b  8855  fzofig  8889  iseqfeq2  8906  expp1  8916  expm1t  8937  expeq0  8940  binom2sub  9017  bernneq  9022  expnlbnd  9026  crim  9086  mulreap  9092  resub  9098  imsub  9106  ipcnval  9114  cjsub  9120  bj-inex  9362  peano5set  9399  findset  9405  bj-findis  9439