Theorem mp3an3 1452

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 1121	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 20	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mp3an13  1454  mp3an23  1455  mp3anl3  1459  el3v3  3453  opelxp  5667  ov  7514  ovmpoa  7525  ovmpo  7530  frecseq123  8239  oaword1  8494  oneo  8523  oeoalem  8538  oeoelem  8540  nnaword1  8571  nnneo  8597  erov  8765  enrefg  8933  f1imaen  8966  mapxpen  9085  0sdom1dom  9163  acnlem  9980  djucomen  10110  nnadju  10130  infmap  10508  canthnumlem  10580  tskin  10691  tsksn  10692  tsk0  10695  gruxp  10739  gruina  10750  genpprecl  10933  addsrpr  11007  mulsrpr  11008  supsrlem  11043  mulrid  11151  00id  11328  mul02lem1  11329  ltneg  11657  leneg  11660  suble0  11671  div1  11851  nnaddcl  12188  nnmulcl  12189  nnge1  12193  nnsub  12209  2halves  12379  halfaddsub  12394  addltmul  12397  fcdmnn0fsuppg  12481  zleltp1  12563  nnaddm1cl  12570  zextlt  12587  eluzp1p1  12800  uzaddcl  12842  znq  12890  xrre  13108  xrre2  13109  fzshftral  13555  fraclt1  13743  expadd  14048  expmul  14051  sqmul  14063  expubnd  14122  bernneq  14173  faclbnd2  14235  faclbnd6  14243  hashgadd  14321  hashun2  14327  hashunsnggt  14338  hashssdif  14356  hashfun  14381  ccatlcan  14661  ccatrcan  14662  pfx2  14891  shftval3  15020  01sqrexlem1  15186  caubnd2  15302  bpoly2  16001  bpoly3  16002  fsumcube  16004  efexp  16047  efival  16098  cos01gt0  16137  odd2np1  16289  halfleoddlt  16310  omoe  16312  opeo  16313  divalglem5  16345  sqgcd  16510  nn0seqcvgd  16518  prmdvdssq  16666  phiprmpw  16724  eulerthlem2  16730  odzcllem  16741  pythagtriplem15  16778  pythagtriplem17  16780  pcelnn  16819  4sqlem3  16899  fullfunc  17852  fthfunc  17853  prfcl  18146  curf1cl  18171  curfcl  18175  hofcl  18202  odinv  19477  lsmelvalix  19557  dprdval  19921  lsp0  20949  lss0v  20957  zndvds0  21494  frlmlbs  21741  lindfres  21767  lmisfree  21786  coe1scl  22208  ntrin  22983  lpsscls  23063  restperf  23106  txuni2  23487  txopn  23524  elqtop2  23623  xkocnv  23736  ptcmp  23980  xblpnfps  24318  xblpnf  24319  bl2in  24323  unirnblps  24342  unirnbl  24343  blpnfctr  24359  dscopn  24496  bcthlem4  25262  minveclem2  25361  minveclem4  25367  icombl  25500  i1fadd  25631  i1fmul  25632  dvn1  25863  dvexp3  25917  plyconst  26146  plyid  26149  sincosq1eq  26456  sinord  26478  cxpp1  26624  cxpsqrtlem  26646  cxpsqrt  26647  angneg  26748  dcubic  26791  issqf  27081  ppiub  27150  bposlem1  27230  bposlem2  27231  bposlem9  27238  nosupno  27650  nosupfv  27653  noinfno  27665  noinffv  27668  scutval  27748  scutun12  27758  cuteq0  27783  cuteq1  27785  cofcut1  27870  cofcutr  27874  addscut2  27928  sleadd1  27938  addsuniflem  27950  addsasslem1  27952  addsasslem2  27953  negscut2  27988  mulsproplem12  28072  mulscut2  28078  divs1  28149  precsexlem10  28160  precsexlem11  28161  bdayon  28215  n0s0suc  28276  nnzsubs  28315  zmulscld  28327  axlowdimlem6  28929  axlowdimlem14  28937  axcontlem2  28947  pthdlem2  29750  0ewlk  30095  ipasslem1  30812  ipasslem2  30813  ipasslem11  30821  minvecolem2  30856  minvecolem3  30857  minvecolem4  30861  shsva  31301  h1datomi  31562  lnfnmuli  32025  leopsq  32110  nmopleid  32120  opsqrlem6  32126  pjnmopi  32129  hstle  32211  csmdsymi  32315  atcvatlem  32366  dpfrac1  32864  cshf1o  32936  cycpmconjslem2  33129  rspidlid  33341  elsx  34179  dya2iocnrect  34267  cvmliftphtlem  35299  satfv1  35345  satffunlem1lem2  35385  satffunlem1  35389  wlimeq12  35802  fvray  36124  fvline  36127  tailfb  36360  uncov  37590  tan2h  37601  matunitlindflem1  37605  matunitlindflem2  37606  poimirlem32  37641  mblfinlem4  37649  mbfresfi  37655  mbfposadd  37656  itg2addnc  37663  ftc1anclem5  37686  ftc1anclem8  37689  dvasin  37693  heiborlem7  37806  igenidl  38052  atlatmstc  39307  dihglblem2N  41283  eldioph4b  42794  diophren  42796  rmxp1  42916  rmyp1  42917  rmxm1  42918  rmym1  42919  dfgric2  47910  gpgov  48028  dig0  48590  i0oii  48903  iinfconstbas  49050  onetansqsecsq  49745  cotsqcscsq  49746