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  3445  opelxp  5655  ov  7493  ovmpoa  7504  ovmpo  7509  frecseq123  8215  oaword1  8470  oneo  8499  oeoalem  8514  oeoelem  8516  nnaword1  8547  nnneo  8573  erov  8741  enrefg  8909  f1imaen  8942  mapxpen  9060  0sdom1dom  9135  acnlem  9942  djucomen  10072  nnadju  10092  infmap  10470  canthnumlem  10542  tskin  10653  tsksn  10654  tsk0  10657  gruxp  10701  gruina  10712  genpprecl  10895  addsrpr  10969  mulsrpr  10970  supsrlem  11005  mulrid  11113  00id  11291  mul02lem1  11292  ltneg  11620  leneg  11623  suble0  11634  div1  11814  nnaddcl  12151  nnmulcl  12152  nnge1  12156  nnsub  12172  2halves  12342  halfaddsub  12357  addltmul  12360  fcdmnn0fsuppg  12444  zleltp1  12526  nnaddm1cl  12533  zextlt  12550  eluzp1p1  12763  uzaddcl  12805  znq  12853  xrre  13071  xrre2  13072  fzshftral  13518  fraclt1  13706  expadd  14011  expmul  14014  sqmul  14026  expubnd  14085  bernneq  14136  faclbnd2  14198  faclbnd6  14206  hashgadd  14284  hashun2  14290  hashunsnggt  14301  hashssdif  14319  hashfun  14344  ccatlcan  14624  ccatrcan  14625  pfx2  14854  shftval3  14983  01sqrexlem1  15149  caubnd2  15265  bpoly2  15964  bpoly3  15965  fsumcube  15967  efexp  16010  efival  16061  cos01gt0  16100  odd2np1  16252  halfleoddlt  16273  omoe  16275  opeo  16276  divalglem5  16308  sqgcd  16473  nn0seqcvgd  16481  prmdvdssq  16629  phiprmpw  16687  eulerthlem2  16693  odzcllem  16704  pythagtriplem15  16741  pythagtriplem17  16743  pcelnn  16782  4sqlem3  16862  fullfunc  17815  fthfunc  17816  prfcl  18109  curf1cl  18134  curfcl  18138  hofcl  18165  odinv  19440  lsmelvalix  19520  dprdval  19884  lsp0  20912  lss0v  20920  zndvds0  21457  frlmlbs  21704  lindfres  21730  lmisfree  21749  coe1scl  22171  ntrin  22946  lpsscls  23026  restperf  23069  txuni2  23450  txopn  23487  elqtop2  23586  xkocnv  23699  ptcmp  23943  xblpnfps  24281  xblpnf  24282  bl2in  24286  unirnblps  24305  unirnbl  24306  blpnfctr  24322  dscopn  24459  bcthlem4  25225  minveclem2  25324  minveclem4  25330  icombl  25463  i1fadd  25594  i1fmul  25595  dvn1  25826  dvexp3  25880  plyconst  26109  plyid  26112  sincosq1eq  26419  sinord  26441  cxpp1  26587  cxpsqrtlem  26609  cxpsqrt  26610  angneg  26711  dcubic  26754  issqf  27044  ppiub  27113  bposlem1  27193  bposlem2  27194  bposlem9  27201  nosupno  27613  nosupfv  27616  noinfno  27628  noinffv  27631  scutval  27712  scutun12  27722  cuteq0  27747  cuteq1  27749  cofcut1  27835  cofcutr  27839  addscut2  27893  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  negscut2  27953  mulsproplem12  28037  mulscut2  28043  divs1  28114  precsexlem10  28125  precsexlem11  28126  bdayon  28180  n0s0suc  28241  nnzsubs  28280  zmulscld  28292  axlowdimlem6  28896  axlowdimlem14  28904  axcontlem2  28914  pthdlem2  29717  0ewlk  30062  ipasslem1  30779  ipasslem2  30780  ipasslem11  30788  minvecolem2  30823  minvecolem3  30824  minvecolem4  30828  shsva  31268  h1datomi  31529  lnfnmuli  31992  leopsq  32077  nmopleid  32087  opsqrlem6  32093  pjnmopi  32096  hstle  32178  csmdsymi  32282  atcvatlem  32333  dpfrac1  32841  cshf1o  32913  cycpmconjslem2  33106  rspidlid  33321  elsx  34177  dya2iocnrect  34265  cvmliftphtlem  35310  satfv1  35356  satffunlem1lem2  35396  satffunlem1  35400  wlimeq12  35813  fvray  36135  fvline  36138  tailfb  36371  uncov  37601  tan2h  37612  matunitlindflem1  37616  matunitlindflem2  37617  poimirlem32  37652  mblfinlem4  37660  mbfresfi  37666  mbfposadd  37667  itg2addnc  37674  ftc1anclem5  37697  ftc1anclem8  37700  dvasin  37704  heiborlem7  37817  igenidl  38063  atlatmstc  39318  dihglblem2N  41293  eldioph4b  42804  diophren  42806  rmxp1  42925  rmyp1  42926  rmxm1  42927  rmym1  42928  dfgric2  47919  gpgov  48046  dig0  48611  i0oii  48924  iinfconstbas  49071  onetansqsecsq  49766  cotsqcscsq  49767