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  6506  genpassu  6507  genpassg  6508  addcomprg  6553  mulcomprg  6555  distrlem1prl  6557  distrlem1pru  6558  1idprl  6565  1idpru  6566  recexprlemdisj  6601  recexprlem1ssl  6604  ax1rid  6741  le2tri3i  6903  add4  6949  cnegexlem1  6963  cnegexlem3  6965  cnegex  6966  subadd  6991  addsub  6999  addsubeq4  7003  negdi  7044  renegcl  7048  resubcl  7051  subdi  7158  mulneg2  7169  mul2neg  7171  submul2  7172  ltnegcon2  7234  lenegcon2  7237  lesub0  7249  cru  7366  recextlem1  7394  recexap  7396  div12ap  7435  divnegap  7445  letrp1  7575  peano2nn  7687  nndivre  7710  nnsub  7713  nndivtr  7716  arch  7934  bndndx  7936  nn0addge1  7984  nn0addge2  7985  zaddcl  8041  zsubcl  8042  zltnle  8047  zrevaddcl  8051  zleltp1  8055  zltlem1  8057  zdiv  8084  peano2uz2  8101  uzind  8105  eluzp1l  8253  ublbneg  8304  qaddcl  8326  qsubcl  8329  qreccl  8331  qdivcl  8332  qrevaddcl  8333  irradd  8335  irrmul  8336  rerpdivcl  8368  xrre  8483  elioc2  8555  icoshft  8608  iccdil  8616  fzss2  8677  fzsuc2  8691  fzrev2  8697  elfzm11  8703  elfzp1b  8709  fzrevral  8717  fzshftral  8720  fzof  8751  fzoval  8755  fzon  8772  fzosubel  8800  zpnn0elfzo  8813  elfzom1b  8835  fzofig  8869  iseqfeq2  8886  expp1  8896  expm1t  8917  expeq0  8920  binom2sub  8997  bernneq  9002  expnlbnd  9006  crim  9066  mulreap  9072  resub  9078  imsub  9086  ipcnval  9094  cjsub  9100  bj-inex  9338  findset  9379  bj-findis  9409