Theorem mp3an3 1451

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 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  mp3an13  1453  mp3an23  1454  mp3anl3  1458  opelxp  5712  ov  7549  ovmpoa  7560  ovmpo  7565  frecseq123  8264  oaword1  8549  oneo  8578  oeoalem  8593  oeoelem  8595  nnaword1  8626  nnneo  8651  erov  8805  enrefg  8977  f1imaen  9009  mapxpen  9140  0sdom1dom  9235  acnlem  10040  djucomen  10169  nnadju  10189  infmap  10568  canthnumlem  10640  tskin  10751  tsksn  10752  tsk0  10755  gruxp  10799  gruina  10810  genpprecl  10993  addsrpr  11067  mulsrpr  11068  supsrlem  11103  mulrid  11209  00id  11386  mul02lem1  11387  ltneg  11711  leneg  11714  suble0  11725  div1  11900  nnaddcl  12232  nnmulcl  12233  nnge1  12237  nnsub  12253  2halves  12437  halfaddsub  12442  addltmul  12445  fcdmnn0fsuppg  12528  zleltp1  12610  nnaddm1cl  12616  zextlt  12633  eluzp1p1  12847  uzaddcl  12885  znq  12933  xrre  13145  xrre2  13146  fzshftral  13586  fraclt1  13764  expadd  14067  expmul  14070  sqmul  14081  expubnd  14139  bernneq  14189  faclbnd2  14248  faclbnd6  14256  hashgadd  14334  hashun2  14340  hashunsnggt  14351  hashssdif  14369  hashfun  14394  ccatlcan  14665  ccatrcan  14666  pfx2  14895  shftval3  15020  01sqrexlem1  15186  caubnd2  15301  bpoly2  15998  bpoly3  15999  fsumcube  16001  efexp  16041  efival  16092  cos01gt0  16131  odd2np1  16281  halfleoddlt  16302  omoe  16304  opeo  16305  divalglem5  16337  sqgcd  16499  nn0seqcvgd  16504  prmdvdssq  16652  phiprmpw  16706  eulerthlem2  16712  odzcllem  16722  pythagtriplem15  16759  pythagtriplem17  16761  pcelnn  16800  4sqlem3  16880  fullfunc  17854  fthfunc  17855  prfcl  18152  curf1cl  18178  curfcl  18182  hofcl  18209  odinv  19424  lsmelvalix  19504  dprdval  19868  lsp0  20613  lss0v  20620  zndvds0  21098  frlmlbs  21344  lindfres  21370  lmisfree  21389  coe1scl  21801  ntrin  22557  lpsscls  22637  restperf  22680  txuni2  23061  txopn  23098  elqtop2  23197  xkocnv  23310  ptcmp  23554  xblpnfps  23893  xblpnf  23894  bl2in  23898  unirnblps  23917  unirnbl  23918  blpnfctr  23934  dscopn  24074  bcthlem4  24836  minveclem2  24935  minveclem4  24941  icombl  25073  i1fadd  25204  i1fmul  25205  dvn1  25435  dvexp3  25487  plyconst  25712  plyid  25715  sincosq1eq  26014  sinord  26035  cxpp1  26180  cxpsqrtlem  26202  cxpsqrt  26203  angneg  26298  dcubic  26341  issqf  26630  ppiub  26697  bposlem1  26777  bposlem2  26778  bposlem9  26785  nosupno  27196  nosupfv  27199  noinfno  27211  noinffv  27214  scutval  27291  scutun12  27301  cuteq0  27323  cuteq1  27324  cofcut1  27397  cofcutr  27401  addscut2  27453  sleadd1  27462  addsuniflem  27474  addsasslem1  27476  addsasslem2  27477  negscut2  27504  mulsproplem12  27573  mulscut2  27579  divs1  27641  precsexlem10  27652  precsexlem11  27653  axlowdimlem6  28195  axlowdimlem14  28203  axcontlem2  28213  pthdlem2  29015  0ewlk  29357  ipasslem1  30072  ipasslem2  30073  ipasslem11  30081  minvecolem2  30116  minvecolem3  30117  minvecolem4  30121  shsva  30561  h1datomi  30822  lnfnmuli  31285  leopsq  31370  nmopleid  31380  opsqrlem6  31386  pjnmopi  31389  hstle  31471  csmdsymi  31575  atcvatlem  31626  dpfrac1  32046  cshf1o  32114  cycpmconjslem2  32302  rspidlid  32476  elsx  33181  dya2iocnrect  33269  cvmliftphtlem  34297  satfv1  34343  satffunlem1lem2  34383  satffunlem1  34387  wlimeq12  34780  fvray  35102  fvline  35105  tailfb  35251  uncov  36458  tan2h  36469  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem32  36509  mblfinlem4  36517  mbfresfi  36523  mbfposadd  36524  itg2addnc  36531  ftc1anclem5  36554  ftc1anclem8  36557  dvasin  36561  heiborlem7  36674  igenidl  36920  el3v3  37078  atlatmstc  38178  dihglblem2N  40154  2xp3dxp2ge1d  41011  factwoffsmonot  41012  eldioph4b  41535  diophren  41537  rmxp1  41657  rmyp1  41658  rmxm1  41659  rmym1  41660  dig0  47246  i0oii  47506  onetansqsecsq  47760  cotsqcscsq  47761