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  7513  ovmpoa  7524  ovmpo  7529  frecseq123  8238  oaword1  8493  oneo  8522  oeoalem  8537  oeoelem  8539  nnaword1  8570  nnneo  8596  erov  8764  enrefg  8932  f1imaen  8965  mapxpen  9084  0sdom1dom  9162  acnlem  9979  djucomen  10109  nnadju  10129  infmap  10507  canthnumlem  10579  tskin  10690  tsksn  10691  tsk0  10694  gruxp  10738  gruina  10749  genpprecl  10932  addsrpr  11006  mulsrpr  11007  supsrlem  11042  mulrid  11150  00id  11327  mul02lem1  11328  ltneg  11656  leneg  11659  suble0  11670  div1  11850  nnaddcl  12187  nnmulcl  12188  nnge1  12192  nnsub  12208  2halves  12378  halfaddsub  12393  addltmul  12396  fcdmnn0fsuppg  12480  zleltp1  12562  nnaddm1cl  12569  zextlt  12586  eluzp1p1  12799  uzaddcl  12841  znq  12889  xrre  13107  xrre2  13108  fzshftral  13554  fraclt1  13742  expadd  14047  expmul  14050  sqmul  14062  expubnd  14121  bernneq  14172  faclbnd2  14234  faclbnd6  14242  hashgadd  14320  hashun2  14326  hashunsnggt  14337  hashssdif  14355  hashfun  14380  ccatlcan  14660  ccatrcan  14661  pfx2  14890  shftval3  15019  01sqrexlem1  15185  caubnd2  15301  bpoly2  16000  bpoly3  16001  fsumcube  16003  efexp  16046  efival  16097  cos01gt0  16136  odd2np1  16288  halfleoddlt  16309  omoe  16311  opeo  16312  divalglem5  16344  sqgcd  16509  nn0seqcvgd  16517  prmdvdssq  16665  phiprmpw  16723  eulerthlem2  16729  odzcllem  16740  pythagtriplem15  16777  pythagtriplem17  16779  pcelnn  16818  4sqlem3  16898  fullfunc  17851  fthfunc  17852  prfcl  18145  curf1cl  18170  curfcl  18174  hofcl  18201  odinv  19476  lsmelvalix  19556  dprdval  19920  lsp0  20948  lss0v  20956  zndvds0  21493  frlmlbs  21740  lindfres  21766  lmisfree  21785  coe1scl  22207  ntrin  22982  lpsscls  23062  restperf  23105  txuni2  23486  txopn  23523  elqtop2  23622  xkocnv  23735  ptcmp  23979  xblpnfps  24317  xblpnf  24318  bl2in  24322  unirnblps  24341  unirnbl  24342  blpnfctr  24358  dscopn  24495  bcthlem4  25261  minveclem2  25360  minveclem4  25366  icombl  25499  i1fadd  25630  i1fmul  25631  dvn1  25862  dvexp3  25916  plyconst  26145  plyid  26148  sincosq1eq  26455  sinord  26477  cxpp1  26623  cxpsqrtlem  26645  cxpsqrt  26646  angneg  26747  dcubic  26790  issqf  27080  ppiub  27149  bposlem1  27229  bposlem2  27230  bposlem9  27237  nosupno  27649  nosupfv  27652  noinfno  27664  noinffv  27667  scutval  27747  scutun12  27757  cuteq0  27782  cuteq1  27784  cofcut1  27869  cofcutr  27873  addscut2  27927  sleadd1  27937  addsuniflem  27949  addsasslem1  27951  addsasslem2  27952  negscut2  27987  mulsproplem12  28071  mulscut2  28077  divs1  28148  precsexlem10  28159  precsexlem11  28160  bdayon  28214  n0s0suc  28275  nnzsubs  28314  zmulscld  28326  axlowdimlem6  28928  axlowdimlem14  28936  axcontlem2  28946  pthdlem2  29749  0ewlk  30094  ipasslem1  30811  ipasslem2  30812  ipasslem11  30820  minvecolem2  30855  minvecolem3  30856  minvecolem4  30860  shsva  31300  h1datomi  31561  lnfnmuli  32024  leopsq  32109  nmopleid  32119  opsqrlem6  32125  pjnmopi  32128  hstle  32210  csmdsymi  32314  atcvatlem  32365  dpfrac1  32863  cshf1o  32935  cycpmconjslem2  33128  rspidlid  33340  elsx  34178  dya2iocnrect  34266  cvmliftphtlem  35298  satfv1  35344  satffunlem1lem2  35384  satffunlem1  35388  wlimeq12  35801  fvray  36123  fvline  36126  tailfb  36359  uncov  37589  tan2h  37600  matunitlindflem1  37604  matunitlindflem2  37605  poimirlem32  37640  mblfinlem4  37648  mbfresfi  37654  mbfposadd  37655  itg2addnc  37662  ftc1anclem5  37685  ftc1anclem8  37688  dvasin  37692  heiborlem7  37805  igenidl  38051  atlatmstc  39306  dihglblem2N  41282  eldioph4b  42793  diophren  42795  rmxp1  42915  rmyp1  42916  rmxm1  42917  rmym1  42918  dfgric2  47909  gpgov  48027  dig0  48589  i0oii  48902  iinfconstbas  49049  onetansqsecsq  49744  cotsqcscsq  49745