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  3451  opelxp  5670  ov  7514  ovmpoa  7525  ovmpo  7530  frecseq123  8236  oaword1  8491  oneo  8520  oeoalem  8536  oeoelem  8538  nnaword1  8569  nnneo  8595  erov  8765  enrefg  8935  f1imaen  8968  mapxpen  9085  0sdom1dom  9160  acnlem  9972  djucomen  10102  nnadju  10122  infmap  10501  canthnumlem  10573  tskin  10684  tsksn  10685  tsk0  10688  gruxp  10732  gruina  10743  genpprecl  10926  addsrpr  11000  mulsrpr  11001  supsrlem  11036  mulrid  11144  00id  11322  mul02lem1  11323  ltneg  11651  leneg  11654  suble0  11665  div1  11845  nnaddcl  12182  nnmulcl  12183  nnge1  12187  nnsub  12203  2halves  12373  halfaddsub  12388  addltmul  12391  fcdmnn0fsuppg  12475  zleltp1  12556  nnaddm1cl  12563  zextlt  12580  eluzp1p1  12793  uzaddcl  12831  znq  12879  xrre  13098  xrre2  13099  fzshftral  13545  fraclt1  13736  expadd  14041  expmul  14044  sqmul  14056  expubnd  14115  bernneq  14166  faclbnd2  14228  faclbnd6  14236  hashgadd  14314  hashun2  14320  hashunsnggt  14331  hashssdif  14349  hashfun  14374  ccatlcan  14655  ccatrcan  14656  pfx2  14884  shftval3  15013  01sqrexlem1  15179  caubnd2  15295  bpoly2  15994  bpoly3  15995  fsumcube  15997  efexp  16040  efival  16091  cos01gt0  16130  odd2np1  16282  halfleoddlt  16303  omoe  16305  opeo  16306  divalglem5  16338  sqgcd  16503  nn0seqcvgd  16511  prmdvdssq  16659  phiprmpw  16717  eulerthlem2  16723  odzcllem  16734  pythagtriplem15  16771  pythagtriplem17  16773  pcelnn  16812  4sqlem3  16892  fullfunc  17846  fthfunc  17847  prfcl  18140  curf1cl  18165  curfcl  18169  hofcl  18196  odinv  19507  lsmelvalix  19587  dprdval  19951  lsp0  20977  lss0v  20985  zndvds0  21522  frlmlbs  21769  lindfres  21795  lmisfree  21814  coe1scl  22246  ntrin  23022  lpsscls  23102  restperf  23145  txuni2  23526  txopn  23563  elqtop2  23662  xkocnv  23775  ptcmp  24019  xblpnfps  24356  xblpnf  24357  bl2in  24361  unirnblps  24380  unirnbl  24381  blpnfctr  24397  dscopn  24534  bcthlem4  25300  minveclem2  25399  minveclem4  25405  icombl  25538  i1fadd  25669  i1fmul  25670  dvn1  25901  dvexp3  25955  plyconst  26184  plyid  26187  sincosq1eq  26494  sinord  26516  cxpp1  26662  cxpsqrtlem  26684  cxpsqrt  26685  angneg  26786  dcubic  26829  issqf  27119  ppiub  27188  bposlem1  27268  bposlem2  27269  bposlem9  27276  nosupno  27688  nosupfv  27691  noinfno  27703  noinffv  27706  cutsval  27793  cutsun12  27803  cuteq0  27828  cuteq1  27830  cofcut1  27933  cofcutr  27937  addcuts2  27992  leadds1  28002  addsuniflem  28014  addsasslem1  28016  addsasslem2  28017  negcut2  28053  mulsproplem12  28140  mulcut2  28146  divs1  28217  precsexlem10  28229  precsexlem11  28230  bdayons  28289  n0s0suc  28355  nnzsubs  28398  zmulscld  28410  elz12si  28486  axlowdimlem6  29038  axlowdimlem14  29046  axcontlem2  29056  pthdlem2  29859  0ewlk  30207  ipasslem1  30925  ipasslem2  30926  ipasslem11  30934  minvecolem2  30969  minvecolem3  30970  minvecolem4  30974  shsva  31414  h1datomi  31675  lnfnmuli  32138  leopsq  32223  nmopleid  32233  opsqrlem6  32239  pjnmopi  32242  hstle  32324  csmdsymi  32428  atcvatlem  32479  dpfrac1  32990  cshf1o  33061  cycpmconjslem2  33255  rspidlid  33474  elsx  34378  dya2iocnrect  34465  r1omhf  35289  cvmliftphtlem  35539  satfv1  35585  satffunlem1lem2  35625  satffunlem1  35629  wlimeq12  36039  fvray  36363  fvline  36366  tailfb  36599  uncov  37881  tan2h  37892  matunitlindflem1  37896  matunitlindflem2  37897  poimirlem32  37932  mblfinlem4  37940  mbfresfi  37946  mbfposadd  37947  itg2addnc  37954  ftc1anclem5  37977  ftc1anclem8  37980  dvasin  37984  heiborlem7  38097  igenidl  38343  atlatmstc  39724  dihglblem2N  41699  eldioph4b  43197  diophren  43199  rmxp1  43318  rmyp1  43319  rmxm1  43320  rmym1  43321  dfgric2  48304  gpgov  48431  dig0  48995  i0oii  49308  iinfconstbas  49454  onetansqsecsq  50149  cotsqcscsq  50150