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  6414  enq0ref  6415  addclnq0  6433  nqpnq0nq  6435  nnanq0  6440  distrnq0  6441  addassnq0lemcl  6443  addassnq0  6444  distnq0r  6445  prarloclemlt  6475  genpassl  6507  genpassu  6508  genpassg  6509  addcomprg  6552  mulcomprg  6554  distrlem1prl  6556  distrlem1pru  6557  1idprl  6564  1idpru  6565  recexprlemdisj  6600  recexprlem1ssl  6603  ax1rid  6721  le2tri3i  6883  add4  6929  cnegexlem1  6943  cnegexlem3  6945  cnegex  6946  subadd  6971  addsub  6979  addsubeq4  6983  negdi  7024  renegcl  7028  resubcl  7031  subdi  7138  mulneg2  7149  mul2neg  7151  submul2  7152  ltnegcon2  7214  lenegcon2  7217  lesub0  7229  cru  7346  recextlem1  7374  recexap  7376  div12ap  7415  divnegap  7425  letrp1  7555  peano2nn  7667  nndivre  7690  nnsub  7693  nndivtr  7696  arch  7914  bndndx  7916  nn0addge1  7964  nn0addge2  7965  zaddcl  8021  zsubcl  8022  zltnle  8027  zrevaddcl  8031  zleltp1  8035  zltlem1  8037  zdiv  8064  peano2uz2  8081  uzind  8085  eluzp1l  8233  ublbneg  8284  qaddcl  8306  qsubcl  8309  qreccl  8311  qdivcl  8312  qrevaddcl  8313  irradd  8315  irrmul  8316  rerpdivcl  8348  xrre  8463  elioc2  8535  icoshft  8588  iccdil  8596  fzss2  8657  fzsuc2  8671  fzrev2  8677  elfzm11  8683  elfzp1b  8689  fzrevral  8697  fzshftral  8700  fzof  8731  fzoval  8735  fzon  8752  fzosubel  8780  zpnn0elfzo  8793  elfzom1b  8815  fzofig  8849  iseqfeq2  8866  expp1  8876  expm1t  8897  expeq0  8900  binom2sub  8977  bernneq  8982  expnlbnd  8986  crim  9046  mulreap  9052  resub  9058  imsub  9066  ipcnval  9074  cjsub  9080  bj-inex  9292  findset  9333  bj-findis  9363