Theorem mp3an3 1452

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  mp3an13  1454  mp3an23  1455  mp3anl3  1459  el3v3  3445  opelxp  5650  ov  7490  ovmpoa  7501  ovmpo  7506  frecseq123  8212  oaword1  8467  oneo  8496  oeoalem  8511  oeoelem  8513  nnaword1  8544  nnneo  8570  erov  8738  enrefg  8906  f1imaen  8939  mapxpen  9056  0sdom1dom  9130  acnlem  9939  djucomen  10069  nnadju  10089  infmap  10467  canthnumlem  10539  tskin  10650  tsksn  10651  tsk0  10654  gruxp  10698  gruina  10709  genpprecl  10892  addsrpr  10966  mulsrpr  10967  supsrlem  11002  mulrid  11110  00id  11288  mul02lem1  11289  ltneg  11617  leneg  11620  suble0  11631  div1  11811  nnaddcl  12148  nnmulcl  12149  nnge1  12153  nnsub  12169  2halves  12339  halfaddsub  12354  addltmul  12357  fcdmnn0fsuppg  12441  zleltp1  12523  nnaddm1cl  12530  zextlt  12547  eluzp1p1  12760  uzaddcl  12802  znq  12850  xrre  13068  xrre2  13069  fzshftral  13515  fraclt1  13706  expadd  14011  expmul  14014  sqmul  14026  expubnd  14085  bernneq  14136  faclbnd2  14198  faclbnd6  14206  hashgadd  14284  hashun2  14290  hashunsnggt  14301  hashssdif  14319  hashfun  14344  ccatlcan  14625  ccatrcan  14626  pfx2  14854  shftval3  14983  01sqrexlem1  15149  caubnd2  15265  bpoly2  15964  bpoly3  15965  fsumcube  15967  efexp  16010  efival  16061  cos01gt0  16100  odd2np1  16252  halfleoddlt  16273  omoe  16275  opeo  16276  divalglem5  16308  sqgcd  16473  nn0seqcvgd  16481  prmdvdssq  16629  phiprmpw  16687  eulerthlem2  16693  odzcllem  16704  pythagtriplem15  16741  pythagtriplem17  16743  pcelnn  16782  4sqlem3  16862  fullfunc  17815  fthfunc  17816  prfcl  18109  curf1cl  18134  curfcl  18138  hofcl  18165  odinv  19473  lsmelvalix  19553  dprdval  19917  lsp0  20942  lss0v  20950  zndvds0  21487  frlmlbs  21734  lindfres  21760  lmisfree  21779  coe1scl  22201  ntrin  22976  lpsscls  23056  restperf  23099  txuni2  23480  txopn  23517  elqtop2  23616  xkocnv  23729  ptcmp  23973  xblpnfps  24310  xblpnf  24311  bl2in  24315  unirnblps  24334  unirnbl  24335  blpnfctr  24351  dscopn  24488  bcthlem4  25254  minveclem2  25353  minveclem4  25359  icombl  25492  i1fadd  25623  i1fmul  25624  dvn1  25855  dvexp3  25909  plyconst  26138  plyid  26141  sincosq1eq  26448  sinord  26470  cxpp1  26616  cxpsqrtlem  26638  cxpsqrt  26639  angneg  26740  dcubic  26783  issqf  27073  ppiub  27142  bposlem1  27222  bposlem2  27223  bposlem9  27230  nosupno  27642  nosupfv  27645  noinfno  27657  noinffv  27660  scutval  27741  scutun12  27751  cuteq0  27776  cuteq1  27778  cofcut1  27864  cofcutr  27868  addscut2  27922  sleadd1  27932  addsuniflem  27944  addsasslem1  27946  addsasslem2  27947  negscut2  27982  mulsproplem12  28066  mulscut2  28072  divs1  28143  precsexlem10  28154  precsexlem11  28155  bdayon  28209  n0s0suc  28270  nnzsubs  28309  zmulscld  28321  axlowdimlem6  28925  axlowdimlem14  28933  axcontlem2  28943  pthdlem2  29746  0ewlk  30094  ipasslem1  30811  ipasslem2  30812  ipasslem11  30820  minvecolem2  30855  minvecolem3  30856  minvecolem4  30860  shsva  31300  h1datomi  31561  lnfnmuli  32024  leopsq  32109  nmopleid  32119  opsqrlem6  32125  pjnmopi  32128  hstle  32210  csmdsymi  32314  atcvatlem  32365  dpfrac1  32872  cshf1o  32943  cycpmconjslem2  33124  rspidlid  33340  elsx  34207  dya2iocnrect  34294  r1omhf  35117  cvmliftphtlem  35361  satfv1  35407  satffunlem1lem2  35447  satffunlem1  35451  wlimeq12  35861  fvray  36185  fvline  36188  tailfb  36421  uncov  37640  tan2h  37651  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem32  37691  mblfinlem4  37699  mbfresfi  37705  mbfposadd  37706  itg2addnc  37713  ftc1anclem5  37736  ftc1anclem8  37739  dvasin  37743  heiborlem7  37856  igenidl  38102  atlatmstc  39417  dihglblem2N  41392  eldioph4b  42903  diophren  42905  rmxp1  43024  rmyp1  43025  rmxm1  43026  rmym1  43027  dfgric2  48014  gpgov  48141  dig0  48706  i0oii  49019  iinfconstbas  49166  onetansqsecsq  49861  cotsqcscsq  49862