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  386  sylanr2  387  mpanr2  416  adantrl  450  adantrr  451  ancom2s  488  3adantr1  1049  3adantr2  1050  3adantr3  1051  syl3anr1  1171  syl3anr3  1173  dfbi3dc  1269  xordidc  1271  elabgt  2657  sbciegft  2766  csbtt  2835  csbnestgf  2871  copsex2t  3952  pofun  4019  onsucmin  4178  onsucelsucr  4179  onsucsssucr  4180  ordsucunielexmid  4196  ordsuc  4221  nlimsucg  4222  elnn  4251  xpsspw  4373  elxp4  4731  elxp5  4732  funimass2  4899  imain  4903  funimaexg  4905  dff1o2  5052  resdif  5069  funbrfv  5133  fvelimab  5150  eqfnfv2  5187  fvimacnvi  5202  ffvresb  5249  fnressn  5270  fmptapd  5275  fnex  5304  rexima  5315  ralima  5316  f1elima  5333  fnotovb  5467  mpt2eq12  5484  fovrn  5562  fnovrn  5567  ofrfval  5639  fnofval  5640  cofunexg  5657  cofunex2g  5658  mpt2exxg  5752  mpt2exg  5753  f1o2ndf1  5768  smodm2  5828  tfrlem9  5853  tfrlemibxssdm  5858  tfri3  5871  rdgruledefgg  5878  frecsuclem1  5899  oav2  5954  oasuc  5955  omv2  5956  onasuc  5957  omsuc  5962  onmsuc  5963  nnaass  5975  nndi  5976  nndir  5980  nnaword  5991  ecelqsg  6066  iinerm  6085  ecovass  6122  ecoviass  6123  ecovdi  6124  ecovidi  6125  addclpi  6181  addasspig  6184  mulasspig  6186  distrpig  6187  mulcanpig  6189  nnppipi  6196  enqdc1  6215  addassnqg  6235  ltbtwnnqq  6266  prarloclemarch  6269  prarloclemarch2  6270  enq0sym  6281  enq0ref  6282  addclnq0  6300  nqpnq0nq  6302  nnanq0  6307  distrnq0  6308  addassnq0lemcl  6310  addassnq0  6311  distnq0r  6312  prarloclemlt  6341  genpassl  6373  genpassu  6374  genpassg  6375  addcomprg  6411  mulcomprg  6413  distrlem1prl  6415  distrlem1pru  6416  1idprl  6423  1idpru  6424  recexprlemdisj  6458  recexprlem1ssl  6461  ax1rid  6565  add4  6759  cnegexlem1  6773  cnegexlem3  6775  cnegex  6776  subadd  6801  addsub  6809  addsubeq4  6813  negdi  6854  renegcl  6858  resubcl  6861  subdi  6968  mulneg2  6979  mul2neg  6981  submul2  6982  ltnegcon2  7044  lenegcon2  7047  bj-inex  7269  findset  7306  bj-findis  7336