Theorem sylan 267

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

Hypotheses

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

Assertion

Ref	Expression
sylan	⊢ ((φ ∧ χ) → θ)

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. 2 ⊢ (φ → ψ)
2		sylan.2	. . 3 ⊢ ((ψ ∧ χ) → θ)
3	2	expcom 109	. 2 ⊢ (χ → (ψ → θ))
4	1, 3	mpan9 265	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:  sylanb  268  sylanbr  269  syl2an  273  sylanl1  382  sylanl2  383  mpanl1  410  mpanl2  411  adantll  445  adantlr  446  ancom1s  503  3adantl1  1059  3adantl2  1060  3adantl3  1061  syl3anl1  1182  syl3anl3  1184  syl3anl  1185  stoic3  1317  eupick  1976  csbiebt  2880  csbnestgf  2892  reuss2  3211  mpteq12  3831  otexg  3958  opelopabt  3990  sonr  4045  sotr  4046  issod  4047  so2nr  4049  so3nr  4050  ordelss  4082  onelon  4087  elrnmpt1s  4527  iota2  4836  funeu  4869  imadif  4922  fnbr  4944  feu  5015  f1ss  5040  f1ssres  5042  dffo2  5053  foco  5059  foun  5088  fun11iun  5090  ffoss  5101  funbrfv  5155  fvco3  5187  fvopab6  5207  funfvbrb  5223  elpreima  5229  ffvelrn  5243  ffvelrnda  5245  dffo4  5258  foelrn  5260  fmptco  5273  fsn2  5280  fvconst2g  5318  fex  5331  funfvima  5333  f1elima  5355  f1ocnvfv1  5360  f1ocnvfv2  5361  cocan2  5371  foeqcnvco  5373  isocnv  5394  isores2  5396  isoini  5400  isoselem  5402  f1oiso  5408  f1ofveu  5443  eloprabga  5533  grprinvlem  5637  suppssof1  5670  ofco  5671  offveqb  5672  fnexALT  5682  f1dmex  5685  ot1stg  5721  ot2ndg  5722  ot3rdgg  5723  eqopi  5740  2ndrn  5751  fo2ndf  5790  smores3  5849  smores2  5850  smoel  5856  smoiso  5858  tfrlem1  5864  tfrlemisucaccv  5880  tfrlemibxssdm  5882  tfrlemiubacc  5885  rdgon  5913  frecrdg  5931  freccl  5932  omv2  5984  nnasuc  5994  nnmsuc  5995  nnacom  6002  nnaass  6003  nnmass  6005  nntri1  6013  nnmordi  6025  swoer  6070  erth  6086  riinerm  6115  qliftlem  6120  ecovass  6151  ecoviass  6152  f1domg  6174  endomtr  6206  xpsnen2g  6239  enen1  6247  enen2  6248  domen1  6249  domen2  6250  addclpi  6311  addasspig  6314  mulasspig  6316  addnidpig  6320  nnppipi  6327  ltanqi  6386  ltmnqi  6387  ltexnqq  6391  archnqq  6400  prarloclemarch2  6402  enq0sym  6414  enq0tr  6416  nqnq0pi  6420  nqnq0  6423  mulcanenq0ec  6427  addclnq0  6433  nqpnq0nq  6435  distrnq0  6441  addassnq0lemcl  6443  addassnq0  6444  prubl  6468  prarloclemlt  6475  genpdf  6490  genipv  6491  genpelvl  6494  genpelvu  6495  genpml  6499  genpmu  6500  genprndl  6503  genprndu  6504  genpassl  6506  genpassu  6507  genpassg  6508  addnqprl  6511  addnqpru  6512  addlocpr  6518  nqprm  6524  nqprl  6532  mulnqprl  6548  mulnqpru  6549  mullocprlem  6550  mullocpr  6551  addcomprg  6553  mulcomprg  6555  distrlem1prl  6557  distrlem1pru  6558  distrlem4prl  6559  distrlem4pru  6560  ltprordil  6564  1idprl  6565  1idpru  6566  ltpopr  6568  ltsopr  6569  ltaddpr  6570  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemlol  6575  ltexprlemopu  6576  ltexprlemupu  6577  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1l  6606  recexprlemss1u  6607  aptiprleml  6610  aptiprlemu  6611  cauappcvgprlemloc  6623  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  00sr  6677  adddir  6796  eqle  6886  le2tri3i  6903  mul4  6922  muladd11  6923  cnegexlem3  6965  addsub12  7001  2addsub  7002  addsubeq4  7003  subadd4  7031  negcon1  7039  negdi2  7045  negsubdi2  7046  neg2sub  7047  renegcl  7048  muladd  7157  subdir  7159  gt0ne0  7197  ltnegcon1  7233  lenegcon1  7236  recexre  7342  ltmul1  7356  recexap  7396  div12ap  7435  p1le  7576  ltmul2  7583  gt0div  7597  ge0div  7598  zlem1lt  8056  nnaddm1cl  8061  zdceq  8072  gtndiv  8091  prime  8093  msqznn  8094  btwnz  8113  uzss  8249  eluzadd  8257  nn0pzuz  8286  divfnzn  8312  qnegcl  8327  qreccl  8331  elico2  8556  iccss  8560  iccsupr  8585  elfz5  8632  fznn  8701  difelfznle  8743  fzoaddel  8798  frec2uzzd  8847  frecuzrdgfn  8859  frecuzrdgcl  8860  frecuzrdgsuc  8862  expap0  8919  mulexp  8928  mulexpzap  8929  expmul  8934  leexp1a  8943  expubnd  8945  zesq  9000  bernneq  9002  bernneq3  9004  crim  9066  mulreap  9072  remul2  9081  immul2  9088  cjexp  9101  absnid  9207  nn0abscl  9209  bj-inex  9338  bj-nn0suc  9394  bj-nn0sucALT  9408