Theorem mp3an3 1480

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an13  1482  mp3an23  1483  mp3anl3  1487  el3v3  3463  opelxp  5691  ov  7585  ovmpoa  7596  ovmpo  7601  frecseq123  8325  oaword1  8585  oneo  8614  oeoalem  8630  oeoelem  8632  nnaword1  8663  nnneo  8689  erov  8860  uncov  8918  enrefg  9036  f1imaen  9069  mapxpen  9187  0sdom1dom  9262  elhf4  9936  acnlem  10151  djucomen  10280  nnadju  10300  infmap  10685  canthnumlem  10757  tskin  10868  tsksn  10869  tsk0  10872  gruxp  10916  gruina  10927  genpprecl  11110  addsrpr  11184  mulsrpr  11185  supsrlem  11220  mulrid  11330  00id  11509  mul02lem1  11510  ltneg  11840  leneg  11843  suble0  11854  div1  12030  nnaddcl  12382  nnmulcl  12383  nnge1  12390  nnsub  12406  2halves  12588  halfaddsub  12603  addltmul  12606  fcdmnn0fsuppg  12690  zleltp1  12771  nnaddm1cl  12780  zextlt  12797  eluzp1p1  13017  uzaddcl  13055  znq  13103  xrre  13323  xrre2  13324  fzshftral  13773  fraclt1  13966  expadd  14271  expmul  14274  sqmul  14286  expubnd  14345  bernneq  14397  faclbnd2  14459  faclbnd6  14467  hashgadd  14545  hashun2  14551  hashunsnggt  14562  hashssdif  14581  hashfun  14606  ccatlcan  14892  ccatrcan  14893  pfx2  15124  shftval3  15255  01sqrexlem1  15435  caubnd2  15551  bpoly2  16249  bpoly3  16250  fsumcube  16252  efexp  16295  efival  16346  cos01gt0  16385  odd2np1  16537  halfleoddlt  16558  omoe  16560  opeo  16561  divalglem5  16593  sqgcd  16762  dvdssqnn  16767  nn0seqcvgd  16771  prmdvdssq  16920  phiprmpw  16979  eulerthlem2  16985  odzcllem  16996  pythagtriplem15  17033  pythagtriplem17  17035  pcelnn  17074  4sqlem3  17154  fullfunc  18109  fthfunc  18110  prfcl  18403  curf1cl  18428  curfcl  18432  hofcl  18459  odinv  19802  lsmelvalix  19882  dprdval  20246  lsp0  21311  lss0v  21318  zndvds0  21883  frlmlbs  22130  lindfres  22156  lmisfree  22175  coe1scl  22633  matunitlindflem1  23021  matunitlindflem2  23022  ntrin  23406  lpsscls  23486  restperf  23529  txuni2  23911  txopn  23948  elqtop2  24047  xkocnv  24160  ptcmp  24404  xblpnfps  24741  xblpnf  24742  bl2in  24746  unirnblps  24765  unirnbl  24766  blpnfctr  24782  dscopn  24919  bcthlem4  25675  minveclem2  25774  minveclem4  25780  icombl  25912  i1fadd  26043  i1fmul  26044  dvn1  26273  dvexp3  26325  plyconst  26551  plyid  26554  sincosq1eq  26868  sinord  26889  cxpp1  27035  cxpsqrtlem  27057  cxpsqrt  27058  angneg  27158  dcubic  27201  issqf  27490  ppiub  27558  bposlem1  27638  bposlem2  27639  bposlem9  27646  nosupno  28087  nosupfv  28090  noinfno  28102  noinffv  28105  cutsval  28193  cutsun12  28203  cuteq0  28228  cuteq1  28230  cofcut1  28333  cofcutr  28337  addcuts2  28392  leadds1  28402  addsuniflem  28414  addsasslem1  28416  addsasslem2  28417  negcut2  28453  mulsproplem12  28540  mulcut2  28546  divs1  28617  precsexlem10  28629  precsexlem11  28630  bdayons  28689  n0s0suc  28755  nnzsubs  28798  zmulscld  28810  elz12si  28886  axlowdimlem6  29552  axlowdimlem14  29560  axcontlem2  29570  pthdlem2  30381  0ewlk  30732  ipasslem1  31460  ipasslem2  31461  ipasslem11  31469  minvecolem2  31504  minvecolem3  31505  minvecolem4  31509  shsva  31949  h1datomi  32210  lnfnmuli  32673  leopsq  32758  nmopleid  32768  opsqrlem6  32774  pjnmopi  32777  hstle  32859  csmdsymi  32963  atcvatlem  33014  dpfrac1  33525  cshf1o  33590  rspidlid  33997  elsx  34894  dya2iocnrect  34980  j0iso  36003  j0ltaleph  36007  cvmliftphtlem  36248  satfv1  36294  satffunlem1lem2  36334  satffunlem1  36338  wlimeq12  36758  fvray  37083  fvline  37086  tailfb  37342  ttc0elw  37492  tan2h  38726  poimirlem32  38761  mblfinlem4  38769  mbfresfi  38775  mbfposadd  38776  itg2addnc  38783  ftc1anclem5  38806  ftc1anclem8  38809  dvasin  38813  heiborlem7  38942  igenidl  39188  atlatmstc  40567  dihglblem2N  42542  eldioph4b  44009  diophren  44011  rmxp1  44130  rmyp1  44131  rmxm1  44132  rmym1  44133  dfgric2  49216  gpgov  49343  dig0  49921  i0oii  50237  iinfconstbas  50383  onetansqsecsq  51132  cotsqcscsq  51133