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  1060  3adantl2  1061  3adantl3  1062  syl3anl1  1183  syl3anl3  1185  syl3anl  1186  stoic3  1320  eupick  1979  csbiebt  2886  csbnestgf  2898  reuss2  3217  mpteq12  3840  otexg  3967  opelopabt  3999  sonr  4054  sotr  4055  issod  4056  so2nr  4058  so3nr  4059  ordelss  4116  onelon  4121  elrnmpt1s  4584  iota2  4893  funeu  4926  imadif  4979  fnbr  5001  feu  5072  f1ss  5097  f1ssres  5099  dffo2  5110  foco  5116  foun  5145  fun11iun  5147  ffoss  5158  funbrfv  5212  fvco3  5244  fvopab6  5264  funfvbrb  5280  elpreima  5286  ffvelrn  5300  ffvelrnda  5302  dffo4  5315  foelrn  5317  fmptco  5330  fsn2  5337  fvconst2g  5375  fex  5388  funfvima  5390  f1elima  5412  f1ocnvfv1  5417  f1ocnvfv2  5418  cocan2  5428  foeqcnvco  5430  isocnv  5451  isores2  5453  isoini  5457  isoselem  5459  f1oiso  5465  f1ofveu  5500  eloprabga  5591  grprinvlem  5695  suppssof1  5728  ofco  5729  offveqb  5730  fnexALT  5740  f1dmex  5743  ot1stg  5779  ot2ndg  5780  ot3rdgg  5781  eqopi  5798  2ndrn  5809  fo2ndf  5848  smores3  5908  smores2  5909  smoel  5915  smoiso  5917  tfrlem1  5923  tfrlemisucaccv  5939  tfrlemibxssdm  5941  tfrlemiubacc  5944  rdgon  5973  frecrdg  5992  freccl  5993  omv2  6045  nnasuc  6055  nnmsuc  6056  nnacom  6063  nnaass  6064  nnmass  6066  nntri1  6074  nnmordi  6089  swoer  6134  erth  6150  riinerm  6179  qliftlem  6184  ecovass  6215  ecoviass  6216  f1domg  6238  endomtr  6270  xpsnen2g  6303  enen1  6311  enen2  6312  domen1  6313  domen2  6314  phplem1  6315  findcard  6345  findcard2  6346  findcard2s  6347  ordiso2  6357  addclpi  6425  addasspig  6428  mulasspig  6430  addnidpig  6434  nnppipi  6441  ltanqi  6500  ltmnqi  6501  ltexnqq  6506  archnqq  6515  prarloclemarch2  6517  enq0sym  6530  enq0tr  6532  nqnq0pi  6536  nqnq0  6539  mulcanenq0ec  6543  addclnq0  6549  nqpnq0nq  6551  distrnq0  6557  addassnq0lemcl  6559  addassnq0  6560  prubl  6584  prarloclemlt  6591  genpdf  6606  genipv  6607  genpelvl  6610  genpelvu  6611  genpml  6615  genpmu  6616  genprndl  6619  genprndu  6620  genpassl  6622  genpassu  6623  genpassg  6624  addnqprl  6627  addnqpru  6628  addlocpr  6634  nqprm  6640  nqprl  6649  nqpru  6650  mulnqprl  6666  mulnqpru  6667  mullocprlem  6668  mullocpr  6669  addcomprg  6676  mulcomprg  6678  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  ltprordil  6687  1idprl  6688  1idpru  6689  ltpopr  6693  ltsopr  6694  ltaddpr  6695  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  prplnqu  6718  recexprlemloc  6729  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  aptiprleml  6737  aptiprlemu  6738  cauappcvgprlemloc  6750  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemloc  6773  caucvgprlemladdrl  6776  caucvgprprlemml  6792  caucvgprprlemloc  6801  00sr  6854  adddir  7018  eqle  7109  le2tri3i  7126  mul4  7145  muladd11  7146  cnegexlem3  7188  addsub12  7224  2addsub  7225  addsubeq4  7226  subadd4  7255  negcon1  7263  negdi2  7269  negsubdi2  7270  neg2sub  7271  renegcl  7272  muladd  7381  subdir  7383  gt0ne0  7422  ltnegcon1  7458  lenegcon1  7461  recexre  7569  ltmul1  7583  recexap  7634  div12ap  7673  p1le  7815  ltmul2  7822  gt0div  7836  ge0div  7837  zlem1lt  8300  nnaddm1cl  8305  zdceq  8316  gtndiv  8335  prime  8337  msqznn  8338  btwnz  8357  uzss  8493  eluzadd  8501  nn0pzuz  8530  divfnzn  8556  qnegcl  8571  qreccl  8576  elico2  8806  iccss  8810  iccsupr  8835  elfz5  8882  fznn  8951  difelfznle  8993  fzoaddel  9048  qdceq  9102  flqbi2  9133  adddivflid  9134  fldivnn0  9137  divfl0  9138  flqmulnn0  9141  fldivnn0le  9145  fldiv4p1lem1div2  9147  ceiqle  9155  flqdiv  9163  modqmulnn  9184  frec2uzzd  9186  frecuzrdgfn  9198  frecuzrdgcl  9199  frecuzrdgsuc  9201  iseqsplit  9238  iseqcaopr2  9241  iseqid  9247  expap0  9285  mulexp  9294  mulexpzap  9295  expmul  9300  leexp1a  9309  expubnd  9311  zesq  9367  bernneq  9369  bernneq3  9371  shftlem  9417  ovshftex  9420  shftval4  9429  shftf  9431  shftcan2  9436  crim  9458  mulreap  9464  remul2  9473  immul2  9480  cjexp  9493  caucvgre  9580  r19.2uz  9591  sqrtsq2  9641  absnid  9671  absexp  9675  nn0abscl  9681  abslt  9684  lenegsq  9691  cau3lem  9710  clim  9802  climshftlemg  9823  climcn1  9829  climcn1lem  9839  clim2iser  9857  clim2iser2  9858  iiserex  9859  iisermulc2  9860  climub  9864  climcaucn  9870  serif0  9871  ialgcvg  9887  ialgcvga  9890  ialgfx  9891  bj-inex  10027  bj-nn0suc  10089  bj-nn0sucALT  10103