Theorem mp3an3 1405

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	⊢ 𝜒
mp3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ 𝜒
2		mp3an3.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expia 1259	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 20	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  mp3an13  1407  mp3an23  1408  mp3anl3  1412  opelxp  5070  ov  6678  ovmpt2a  6689  ovmpt2  6694  oaword1  7519  oneo  7548  oeoalem  7563  oeoelem  7565  nnaword1  7596  nnneo  7618  erov  7731  enrefg  7873  f1imaen  7904  mapxpen  8011  acnlem  8754  cdacomen  8886  infmap  9277  canthnumlem  9349  tskin  9460  tsksn  9461  tsk0  9464  gruxp  9508  gruina  9519  genpprecl  9702  addsrpr  9775  mulsrpr  9776  supsrlem  9811  mulid1  9916  00id  10090  mul02lem1  10091  ltneg  10407  leneg  10410  suble0  10421  div1  10595  nnaddcl  10919  nnmulcl  10920  nnge1  10923  nnsub  10936  2halves  11137  halfaddsub  11142  addltmul  11145  zleltp1  11305  nnaddm1cl  11311  zextlt  11327  eluzp1p1  11589  uzaddcl  11620  znq  11668  xrre  11874  xrre2  11875  fzshftral  12297  fraclt1  12465  expadd  12764  expmul  12767  expubnd  12783  sqmul  12788  bernneq  12852  faclbnd2  12940  faclbnd6  12948  hashgadd  13027  hashun2  13033  hashssdif  13061  hashfun  13084  ccatlcan  13324  ccatrcan  13325  shftval3  13664  sqrlem1  13831  caubnd2  13945  bpoly2  14627  bpoly3  14628  fsumcube  14630  efexp  14670  efival  14721  cos01gt0  14760  odd2np1  14903  halfleoddlt  14924  omoe  14926  opeo  14927  divalglem5  14958  gcdmultiple  15107  sqgcd  15116  nn0seqcvgd  15121  phiprmpw  15319  eulerthlem2  15325  odzcllem  15335  pythagtriplem15  15372  pythagtriplem17  15374  pcelnn  15412  4sqlem3  15492  xpscfn  16042  fullfunc  16389  fthfunc  16390  prfcl  16666  curf1cl  16691  curfcl  16695  hofcl  16722  odinv  17801  lsmelvalix  17879  dprdval  18225  lsp0  18830  lss0v  18837  coe1scl  19478  zndvds0  19718  frlmlbs  19955  lindfres  19981  lmisfree  20000  ntrin  20675  lpsscls  20755  restperf  20798  txuni2  21178  txopn  21215  elqtop2  21314  xkocnv  21427  ptcmp  21672  xblpnfps  22010  xblpnf  22011  bl2in  22015  unirnblps  22034  unirnbl  22035  blpnfctr  22051  dscopn  22188  bcthlem4  22932  minveclem2  23005  minveclem4  23011  icombl  23139  i1fadd  23268  i1fmul  23269  dvn1  23495  dvexp3  23545  plyconst  23766  plyid  23769  sincosq1eq  24068  sinord  24084  cxpp1  24226  cxpsqrtlem  24248  cxpsqrt  24249  angneg  24333  dcubic  24373  issqf  24662  ppiub  24729  bposlem1  24809  bposlem2  24810  bposlem9  24817  axlowdimlem6  25627  axlowdimlem14  25635  axcontlem2  25645  structgrssvtxlem  25700  wwlkn0s  26233  clwwlkn2  26303  rusgranumwlkb0  26480  ipasslem1  27070  ipasslem2  27071  ipasslem11  27079  minvecolem2  27115  minvecolem3  27116  minvecolem4  27120  shsva  27563  h1datomi  27824  lnfnmuli  28287  leopsq  28372  nmopleid  28382  opsqrlem6  28388  pjnmopi  28391  hstle  28473  csmdsymi  28577  atcvatlem  28628  elsx  29584  dya2iocnrect  29670  cvmliftphtlem  30553  wlimeq12  31009  nofulllem4  31104  fvray  31418  fvline  31421  tailfb  31542  uncov  32560  tan2h  32571  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem32  32611  mblfinlem4  32619  mbfresfi  32626  mbfposadd  32627  itg2addnc  32634  ftc1anclem5  32659  ftc1anclem8  32662  dvasin  32666  heiborlem7  32786  igenidl  33032  atlatmstc  33624  dihglblem2N  35601  eldioph4b  36393  diophren  36395  rmxp1  36515  rmyp1  36516  rmxm1  36517  rmym1  36518  wepwso  36631  pfx2  40275  pthdlem2  40974  0ewlk  41282  dig0  42198  onetansqsecsq  42301  cotsqcscsq  42302  dpfrac1  42312  dpfrac1OLD  42313