Theorem mp3an3 1459

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  mp3an13  1461  mp3an23  1462  mp3anl3  1466  el3v3  3442  opelxp  5656  ov  7503  ovmpoa  7514  ovmpo  7519  frecseq123  8225  oaword1  8481  oneo  8510  oeoalem  8526  oeoelem  8528  nnaword1  8559  nnneo  8585  erov  8755  enrefg  8925  f1imaen  8958  mapxpen  9075  0sdom1dom  9150  acnlem  9965  djucomen  10095  nnadju  10115  infmap  10495  canthnumlem  10567  tskin  10678  tsksn  10679  tsk0  10682  gruxp  10726  gruina  10737  genpprecl  10920  addsrpr  10994  mulsrpr  10995  supsrlem  11030  mulrid  11138  00id  11317  mul02lem1  11318  ltneg  11646  leneg  11649  suble0  11660  div1  11839  nnaddcl  12192  nnmulcl  12193  nnge1  12200  nnsub  12216  2halves  12390  halfaddsub  12405  addltmul  12408  fcdmnn0fsuppg  12492  zleltp1  12573  nnaddm1cl  12581  zextlt  12598  eluzp1p1  12811  uzaddcl  12849  znq  12897  xrre  13116  xrre2  13117  fzshftral  13564  fraclt1  13756  expadd  14061  expmul  14064  sqmul  14076  expubnd  14135  bernneq  14186  faclbnd2  14248  faclbnd6  14256  hashgadd  14334  hashun2  14340  hashunsnggt  14351  hashssdif  14369  hashfun  14394  ccatlcan  14675  ccatrcan  14676  pfx2  14904  shftval3  15033  01sqrexlem1  15199  caubnd2  15315  bpoly2  16017  bpoly3  16018  fsumcube  16020  efexp  16063  efival  16114  cos01gt0  16153  odd2np1  16305  halfleoddlt  16326  omoe  16328  opeo  16329  divalglem5  16361  sqgcd  16526  nn0seqcvgd  16534  prmdvdssq  16683  phiprmpw  16741  eulerthlem2  16747  odzcllem  16758  pythagtriplem15  16795  pythagtriplem17  16797  pcelnn  16836  4sqlem3  16916  fullfunc  17870  fthfunc  17871  prfcl  18164  curf1cl  18189  curfcl  18193  hofcl  18220  odinv  19530  lsmelvalix  19610  dprdval  19974  lsp0  21002  lss0v  21009  zndvds0  21528  frlmlbs  21775  lindfres  21801  lmisfree  21820  coe1scl  22276  ntrin  23047  lpsscls  23127  restperf  23170  txuni2  23551  txopn  23588  elqtop2  23687  xkocnv  23800  ptcmp  24044  xblpnfps  24381  xblpnf  24382  bl2in  24386  unirnblps  24405  unirnbl  24406  blpnfctr  24422  dscopn  24559  bcthlem4  25315  minveclem2  25414  minveclem4  25420  icombl  25552  i1fadd  25683  i1fmul  25684  dvn1  25914  dvexp3  25966  plyconst  26192  plyid  26195  sincosq1eq  26497  sinord  26519  cxpp1  26665  cxpsqrtlem  26687  cxpsqrt  26688  angneg  26788  dcubic  26831  issqf  27120  ppiub  27188  bposlem1  27268  bposlem2  27269  bposlem9  27276  nosupno  27687  nosupfv  27690  noinfno  27702  noinffv  27705  cutsval  27792  cutsun12  27802  cuteq0  27827  cuteq1  27829  cofcut1  27932  cofcutr  27936  addcuts2  27991  leadds1  28001  addsuniflem  28013  addsasslem1  28015  addsasslem2  28016  negcut2  28052  mulsproplem12  28139  mulcut2  28145  divs1  28216  precsexlem10  28228  precsexlem11  28229  bdayons  28288  n0s0suc  28354  nnzsubs  28397  zmulscld  28409  elz12si  28485  axlowdimlem6  29036  axlowdimlem14  29044  axcontlem2  29054  pthdlem2  29856  0ewlk  30204  ipasslem1  30922  ipasslem2  30923  ipasslem11  30931  minvecolem2  30966  minvecolem3  30967  minvecolem4  30971  shsva  31411  h1datomi  31672  lnfnmuli  32135  leopsq  32220  nmopleid  32230  opsqrlem6  32236  pjnmopi  32239  hstle  32321  csmdsymi  32425  atcvatlem  32476  dpfrac1  32972  cshf1o  33043  cycpmconjslem2  33238  rspidlid  33460  elsx  34388  dya2iocnrect  34475  r1omhf  35300  cvmliftphtlem  35558  satfv1  35604  satffunlem1lem2  35644  satffunlem1  35648  wlimeq12  36058  fvray  36382  fvline  36385  tailfb  36618  ttc0elw  36768  uncov  37981  tan2h  37992  matunitlindflem1  37996  matunitlindflem2  37997  poimirlem32  38032  mblfinlem4  38040  mbfresfi  38046  mbfposadd  38047  itg2addnc  38054  ftc1anclem5  38077  ftc1anclem8  38080  dvasin  38084  heiborlem7  38197  igenidl  38443  atlatmstc  39824  dihglblem2N  41799  eldioph4b  43269  diophren  43271  rmxp1  43390  rmyp1  43391  rmxm1  43392  rmym1  43393  dfgric2  48418  gpgov  48545  dig0  49109  i0oii  49422  iinfconstbas  49568  onetansqsecsq  50263  cotsqcscsq  50264