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  3439  opelxp  5658  ov  7502  ovmpoa  7513  ovmpo  7518  frecseq123  8223  oaword1  8478  oneo  8507  oeoalem  8523  oeoelem  8525  nnaword1  8556  nnneo  8582  erov  8752  enrefg  8922  f1imaen  8955  mapxpen  9072  0sdom1dom  9147  acnlem  9959  djucomen  10089  nnadju  10109  infmap  10488  canthnumlem  10560  tskin  10671  tsksn  10672  tsk0  10675  gruxp  10719  gruina  10730  genpprecl  10913  addsrpr  10987  mulsrpr  10988  supsrlem  11023  mulrid  11131  00id  11309  mul02lem1  11310  ltneg  11638  leneg  11641  suble0  11652  div1  11832  nnaddcl  12169  nnmulcl  12170  nnge1  12174  nnsub  12190  2halves  12360  halfaddsub  12375  addltmul  12378  fcdmnn0fsuppg  12462  zleltp1  12543  nnaddm1cl  12550  zextlt  12567  eluzp1p1  12780  uzaddcl  12818  znq  12866  xrre  13085  xrre2  13086  fzshftral  13532  fraclt1  13723  expadd  14028  expmul  14031  sqmul  14043  expubnd  14102  bernneq  14153  faclbnd2  14215  faclbnd6  14223  hashgadd  14301  hashun2  14307  hashunsnggt  14318  hashssdif  14336  hashfun  14361  ccatlcan  14642  ccatrcan  14643  pfx2  14871  shftval3  15000  01sqrexlem1  15166  caubnd2  15282  bpoly2  15981  bpoly3  15982  fsumcube  15984  efexp  16027  efival  16078  cos01gt0  16117  odd2np1  16269  halfleoddlt  16290  omoe  16292  opeo  16293  divalglem5  16325  sqgcd  16490  nn0seqcvgd  16498  prmdvdssq  16646  phiprmpw  16704  eulerthlem2  16710  odzcllem  16721  pythagtriplem15  16758  pythagtriplem17  16760  pcelnn  16799  4sqlem3  16879  fullfunc  17833  fthfunc  17834  prfcl  18127  curf1cl  18152  curfcl  18156  hofcl  18183  odinv  19494  lsmelvalix  19574  dprdval  19938  lsp0  20962  lss0v  20970  zndvds0  21507  frlmlbs  21754  lindfres  21780  lmisfree  21799  coe1scl  22230  ntrin  23004  lpsscls  23084  restperf  23127  txuni2  23508  txopn  23545  elqtop2  23644  xkocnv  23757  ptcmp  24001  xblpnfps  24338  xblpnf  24339  bl2in  24343  unirnblps  24362  unirnbl  24363  blpnfctr  24379  dscopn  24516  bcthlem4  25272  minveclem2  25371  minveclem4  25377  icombl  25509  i1fadd  25640  i1fmul  25641  dvn1  25871  dvexp3  25923  plyconst  26152  plyid  26155  sincosq1eq  26461  sinord  26483  cxpp1  26629  cxpsqrtlem  26651  cxpsqrt  26652  angneg  26753  dcubic  26796  issqf  27086  ppiub  27155  bposlem1  27235  bposlem2  27236  bposlem9  27243  nosupno  27655  nosupfv  27658  noinfno  27670  noinffv  27673  cutsval  27760  cutsun12  27770  cuteq0  27795  cuteq1  27797  cofcut1  27900  cofcutr  27904  addcuts2  27959  leadds1  27969  addsuniflem  27981  addsasslem1  27983  addsasslem2  27984  negcut2  28020  mulsproplem12  28107  mulcut2  28113  divs1  28184  precsexlem10  28196  precsexlem11  28197  bdayons  28256  n0s0suc  28322  nnzsubs  28365  zmulscld  28377  elz12si  28453  axlowdimlem6  29004  axlowdimlem14  29012  axcontlem2  29022  pthdlem2  29825  0ewlk  30173  ipasslem1  30891  ipasslem2  30892  ipasslem11  30900  minvecolem2  30935  minvecolem3  30936  minvecolem4  30940  shsva  31380  h1datomi  31641  lnfnmuli  32104  leopsq  32189  nmopleid  32199  opsqrlem6  32205  pjnmopi  32208  hstle  32290  csmdsymi  32394  atcvatlem  32445  dpfrac1  32956  cshf1o  33027  cycpmconjslem2  33221  rspidlid  33440  elsx  34344  dya2iocnrect  34431  r1omhf  35255  cvmliftphtlem  35505  satfv1  35551  satffunlem1lem2  35591  satffunlem1  35595  wlimeq12  36005  fvray  36329  fvline  36332  tailfb  36565  ttc0elw  36715  uncov  37913  tan2h  37924  matunitlindflem1  37928  matunitlindflem2  37929  poimirlem32  37964  mblfinlem4  37972  mbfresfi  37978  mbfposadd  37979  itg2addnc  37986  ftc1anclem5  38009  ftc1anclem8  38012  dvasin  38016  heiborlem7  38129  igenidl  38375  atlatmstc  39756  dihglblem2N  41731  eldioph4b  43242  diophren  43244  rmxp1  43363  rmyp1  43364  rmxm1  43365  rmym1  43366  dfgric2  48349  gpgov  48476  dig0  49040  i0oii  49353  iinfconstbas  49499  onetansqsecsq  50194  cotsqcscsq  50195