Theorem mp3an3 1453

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

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

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 1089

This theorem is referenced by:  mp3an13  1455  mp3an23  1456  mp3anl3  1460  el3v3  3450  opelxp  5661  ov  7505  ovmpoa  7516  ovmpo  7521  frecseq123  8227  oaword1  8482  oneo  8511  oeoalem  8527  oeoelem  8529  nnaword1  8560  nnneo  8586  erov  8756  enrefg  8926  f1imaen  8959  mapxpen  9076  0sdom1dom  9151  acnlem  9963  djucomen  10093  nnadju  10113  infmap  10492  canthnumlem  10564  tskin  10675  tsksn  10676  tsk0  10679  gruxp  10723  gruina  10734  genpprecl  10917  addsrpr  10991  mulsrpr  10992  supsrlem  11027  mulrid  11135  00id  11313  mul02lem1  11314  ltneg  11642  leneg  11645  suble0  11656  div1  11836  nnaddcl  12173  nnmulcl  12174  nnge1  12178  nnsub  12194  2halves  12364  halfaddsub  12379  addltmul  12382  fcdmnn0fsuppg  12466  zleltp1  12547  nnaddm1cl  12554  zextlt  12571  eluzp1p1  12784  uzaddcl  12822  znq  12870  xrre  13089  xrre2  13090  fzshftral  13536  fraclt1  13727  expadd  14032  expmul  14035  sqmul  14047  expubnd  14106  bernneq  14157  faclbnd2  14219  faclbnd6  14227  hashgadd  14305  hashun2  14311  hashunsnggt  14322  hashssdif  14340  hashfun  14365  ccatlcan  14646  ccatrcan  14647  pfx2  14875  shftval3  15004  01sqrexlem1  15170  caubnd2  15286  bpoly2  15985  bpoly3  15986  fsumcube  15988  efexp  16031  efival  16082  cos01gt0  16121  odd2np1  16273  halfleoddlt  16294  omoe  16296  opeo  16297  divalglem5  16329  sqgcd  16494  nn0seqcvgd  16502  prmdvdssq  16650  phiprmpw  16708  eulerthlem2  16714  odzcllem  16725  pythagtriplem15  16762  pythagtriplem17  16764  pcelnn  16803  4sqlem3  16883  fullfunc  17837  fthfunc  17838  prfcl  18131  curf1cl  18156  curfcl  18160  hofcl  18187  odinv  19495  lsmelvalix  19575  dprdval  19939  lsp0  20965  lss0v  20973  zndvds0  21510  frlmlbs  21757  lindfres  21783  lmisfree  21802  coe1scl  22234  ntrin  23010  lpsscls  23090  restperf  23133  txuni2  23514  txopn  23551  elqtop2  23650  xkocnv  23763  ptcmp  24007  xblpnfps  24344  xblpnf  24345  bl2in  24349  unirnblps  24368  unirnbl  24369  blpnfctr  24385  dscopn  24522  bcthlem4  25288  minveclem2  25387  minveclem4  25393  icombl  25526  i1fadd  25657  i1fmul  25658  dvn1  25889  dvexp3  25943  plyconst  26172  plyid  26175  sincosq1eq  26482  sinord  26504  cxpp1  26650  cxpsqrtlem  26672  cxpsqrt  26673  angneg  26774  dcubic  26817  issqf  27107  ppiub  27176  bposlem1  27256  bposlem2  27257  bposlem9  27264  nosupno  27676  nosupfv  27679  noinfno  27691  noinffv  27694  cutsval  27781  cutsun12  27791  cuteq0  27816  cuteq1  27818  cofcut1  27921  cofcutr  27925  addcuts2  27980  leadds1  27990  addsuniflem  28002  addsasslem1  28004  addsasslem2  28005  negcut2  28041  mulsproplem12  28128  mulcut2  28134  divs1  28205  precsexlem10  28217  precsexlem11  28218  bdayons  28277  n0s0suc  28343  nnzsubs  28386  zmulscld  28398  elz12si  28474  axlowdimlem6  29025  axlowdimlem14  29033  axcontlem2  29043  pthdlem2  29846  0ewlk  30194  ipasslem1  30911  ipasslem2  30912  ipasslem11  30920  minvecolem2  30955  minvecolem3  30956  minvecolem4  30960  shsva  31400  h1datomi  31661  lnfnmuli  32124  leopsq  32209  nmopleid  32219  opsqrlem6  32225  pjnmopi  32228  hstle  32310  csmdsymi  32414  atcvatlem  32465  dpfrac1  32976  cshf1o  33047  cycpmconjslem2  33241  rspidlid  33460  elsx  34364  dya2iocnrect  34451  r1omhf  35275  cvmliftphtlem  35524  satfv1  35570  satffunlem1lem2  35610  satffunlem1  35614  wlimeq12  36024  fvray  36348  fvline  36351  tailfb  36584  uncov  37815  tan2h  37826  matunitlindflem1  37830  matunitlindflem2  37831  poimirlem32  37866  mblfinlem4  37874  mbfresfi  37880  mbfposadd  37881  itg2addnc  37888  ftc1anclem5  37911  ftc1anclem8  37914  dvasin  37918  heiborlem7  38031  igenidl  38277  atlatmstc  39658  dihglblem2N  41633  eldioph4b  43131  diophren  43133  rmxp1  43252  rmyp1  43253  rmxm1  43254  rmym1  43255  dfgric2  48238  gpgov  48365  dig0  48929  i0oii  49242  iinfconstbas  49388  onetansqsecsq  50083  cotsqcscsq  50084