Theorem mp3an3 1449

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 1120	. 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  1451  mp3an23  1452  mp3anl3  1456  el3v3  3486  opelxp  5724  ov  7576  ovmpoa  7587  ovmpo  7592  frecseq123  8305  oaword1  8588  oneo  8617  oeoalem  8632  oeoelem  8634  nnaword1  8665  nnneo  8691  erov  8852  enrefg  9022  f1imaen  9055  mapxpen  9181  0sdom1dom  9271  acnlem  10085  djucomen  10215  nnadju  10235  infmap  10613  canthnumlem  10685  tskin  10796  tsksn  10797  tsk0  10800  gruxp  10844  gruina  10855  genpprecl  11038  addsrpr  11112  mulsrpr  11113  supsrlem  11148  mulrid  11256  00id  11433  mul02lem1  11434  ltneg  11760  leneg  11763  suble0  11774  div1  11954  nnaddcl  12286  nnmulcl  12287  nnge1  12291  nnsub  12307  2halves  12491  halfaddsub  12496  addltmul  12499  fcdmnn0fsuppg  12583  zleltp1  12665  nnaddm1cl  12672  zextlt  12689  eluzp1p1  12903  uzaddcl  12943  znq  12991  xrre  13207  xrre2  13208  fzshftral  13651  fraclt1  13838  expadd  14141  expmul  14144  sqmul  14155  expubnd  14213  bernneq  14264  faclbnd2  14326  faclbnd6  14334  hashgadd  14412  hashun2  14418  hashunsnggt  14429  hashssdif  14447  hashfun  14472  ccatlcan  14752  ccatrcan  14753  pfx2  14982  shftval3  15111  01sqrexlem1  15277  caubnd2  15392  bpoly2  16089  bpoly3  16090  fsumcube  16092  efexp  16133  efival  16184  cos01gt0  16223  odd2np1  16374  halfleoddlt  16395  omoe  16397  opeo  16398  divalglem5  16430  sqgcd  16595  nn0seqcvgd  16603  prmdvdssq  16751  phiprmpw  16809  eulerthlem2  16815  odzcllem  16825  pythagtriplem15  16862  pythagtriplem17  16864  pcelnn  16903  4sqlem3  16983  fullfunc  17959  fthfunc  17960  prfcl  18258  curf1cl  18284  curfcl  18288  hofcl  18315  odinv  19593  lsmelvalix  19673  dprdval  20037  lsp0  21024  lss0v  21032  zndvds0  21586  frlmlbs  21834  lindfres  21860  lmisfree  21879  coe1scl  22305  ntrin  23084  lpsscls  23164  restperf  23207  txuni2  23588  txopn  23625  elqtop2  23724  xkocnv  23837  ptcmp  24081  xblpnfps  24420  xblpnf  24421  bl2in  24425  unirnblps  24444  unirnbl  24445  blpnfctr  24461  dscopn  24601  bcthlem4  25374  minveclem2  25473  minveclem4  25479  icombl  25612  i1fadd  25743  i1fmul  25744  dvn1  25976  dvexp3  26030  plyconst  26259  plyid  26262  sincosq1eq  26568  sinord  26590  cxpp1  26736  cxpsqrtlem  26758  cxpsqrt  26759  angneg  26860  dcubic  26903  issqf  27193  ppiub  27262  bposlem1  27342  bposlem2  27343  bposlem9  27350  nosupno  27762  nosupfv  27765  noinfno  27777  noinffv  27780  scutval  27859  scutun12  27869  cuteq0  27891  cuteq1  27892  cofcut1  27968  cofcutr  27972  addscut2  28026  sleadd1  28036  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  negscut2  28086  mulsproplem12  28167  mulscut2  28173  divs1  28243  precsexlem10  28254  precsexlem11  28255  n0s0suc  28359  nnzsubs  28385  zmulscld  28397  axlowdimlem6  28976  axlowdimlem14  28984  axcontlem2  28994  pthdlem2  29800  0ewlk  30142  ipasslem1  30859  ipasslem2  30860  ipasslem11  30868  minvecolem2  30903  minvecolem3  30904  minvecolem4  30908  shsva  31348  h1datomi  31609  lnfnmuli  32072  leopsq  32157  nmopleid  32167  opsqrlem6  32173  pjnmopi  32176  hstle  32258  csmdsymi  32362  atcvatlem  32413  dpfrac1  32858  cshf1o  32931  cycpmconjslem2  33157  rspidlid  33382  elsx  34174  dya2iocnrect  34262  cvmliftphtlem  35301  satfv1  35347  satffunlem1lem2  35387  satffunlem1  35391  wlimeq12  35800  fvray  36122  fvline  36125  tailfb  36359  uncov  37587  tan2h  37598  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem32  37638  mblfinlem4  37646  mbfresfi  37652  mbfposadd  37653  itg2addnc  37660  ftc1anclem5  37683  ftc1anclem8  37686  dvasin  37690  heiborlem7  37803  igenidl  38049  atlatmstc  39300  dihglblem2N  41276  2xp3dxp2ge1d  42222  factwoffsmonot  42223  eldioph4b  42798  diophren  42800  rmxp1  42920  rmyp1  42921  rmxm1  42922  rmym1  42923  dfgric2  47821  gpgov  47936  dig0  48455  i0oii  48715  onetansqsecsq  48991  cotsqcscsq  48992