Theorem mp3an3 1447

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  mp3an13  1449  mp3an23  1450  mp3anl3  1454  opelxp  5555  ov  7273  ovmpoa  7284  ovmpo  7289  oaword1  8161  oneo  8190  oeoalem  8205  oeoelem  8207  nnaword1  8238  nnneo  8261  erov  8377  enrefg  8524  f1imaen  8554  mapxpen  8667  acnlem  9459  djucomen  9588  nnadju  9608  infmap  9987  canthnumlem  10059  tskin  10170  tsksn  10171  tsk0  10174  gruxp  10218  gruina  10229  genpprecl  10412  addsrpr  10486  mulsrpr  10487  supsrlem  10522  mulid1  10628  00id  10804  mul02lem1  10805  ltneg  11129  leneg  11132  suble0  11143  div1  11318  nnaddcl  11648  nnmulcl  11649  nnge1  11653  nnsub  11669  2halves  11853  halfaddsub  11858  addltmul  11861  zleltp1  12021  nnaddm1cl  12027  zextlt  12044  eluzp1p1  12258  uzaddcl  12292  znq  12340  xrre  12550  xrre2  12551  fzshftral  12990  fraclt1  13167  expadd  13467  expmul  13470  sqmul  13481  expubnd  13537  bernneq  13586  faclbnd2  13647  faclbnd6  13655  hashgadd  13734  hashun2  13740  hashunsnggt  13751  hashssdif  13769  hashfun  13794  ccatlcan  14071  ccatrcan  14072  pfx2  14300  shftval3  14427  sqrlem1  14594  caubnd2  14709  bpoly2  15403  bpoly3  15404  fsumcube  15406  efexp  15446  efival  15497  cos01gt0  15536  odd2np1  15682  halfleoddlt  15703  omoe  15705  opeo  15706  divalglem5  15738  gcdmultipleOLD  15890  sqgcd  15899  nn0seqcvgd  15904  phiprmpw  16103  eulerthlem2  16109  odzcllem  16119  pythagtriplem15  16156  pythagtriplem17  16158  pcelnn  16196  4sqlem3  16276  fullfunc  17168  fthfunc  17169  prfcl  17445  curf1cl  17470  curfcl  17474  hofcl  17501  odinv  18680  lsmelvalix  18758  dprdval  19118  lsp0  19774  lss0v  19781  zndvds0  20242  frlmlbs  20486  lindfres  20512  lmisfree  20531  coe1scl  20916  ntrin  21666  lpsscls  21746  restperf  21789  txuni2  22170  txopn  22207  elqtop2  22306  xkocnv  22419  ptcmp  22663  xblpnfps  23002  xblpnf  23003  bl2in  23007  unirnblps  23026  unirnbl  23027  blpnfctr  23043  dscopn  23180  bcthlem4  23931  minveclem2  24030  minveclem4  24036  icombl  24168  i1fadd  24299  i1fmul  24300  dvn1  24529  dvexp3  24581  plyconst  24803  plyid  24806  sincosq1eq  25105  sinord  25126  cxpp1  25271  cxpsqrtlem  25293  cxpsqrt  25294  angneg  25389  dcubic  25432  issqf  25721  ppiub  25788  bposlem1  25868  bposlem2  25869  bposlem9  25876  axlowdimlem6  26741  axlowdimlem14  26749  axcontlem2  26759  pthdlem2  27557  0ewlk  27899  ipasslem1  28614  ipasslem2  28615  ipasslem11  28623  minvecolem2  28658  minvecolem3  28659  minvecolem4  28663  shsva  29103  h1datomi  29364  lnfnmuli  29827  leopsq  29912  nmopleid  29922  opsqrlem6  29928  pjnmopi  29931  hstle  30013  csmdsymi  30117  atcvatlem  30168  dpfrac1  30594  cshf1o  30662  cycpmconjslem2  30847  rspidlid  30990  elsx  31563  dya2iocnrect  31649  cvmliftphtlem  32677  satfv1  32723  satffunlem1lem2  32763  satffunlem1  32767  wlimeq12  33219  frecseq123  33232  nosupno  33316  nosupfv  33319  scutval  33378  scutun12  33384  fvray  33715  fvline  33718  tailfb  33838  uncov  35038  tan2h  35049  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem32  35089  mblfinlem4  35097  mbfresfi  35103  mbfposadd  35104  itg2addnc  35111  ftc1anclem5  35134  ftc1anclem8  35137  dvasin  35141  heiborlem7  35255  igenidl  35501  el3v3  35654  atlatmstc  36615  dihglblem2N  38590  2xp3dxp2ge1d  39387  factwoffsmonot  39388  eldioph4b  39752  diophren  39754  rmxp1  39873  rmyp1  39874  rmxm1  39875  rmym1  39876  wepwso  39987  dig0  45020  onetansqsecsq  45287  cotsqcscsq  45288