Theorem mp3an3 1448

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  mp3an13  1450  mp3an23  1451  mp3anl3  1455  opelxp  5711  ov  7554  ovmpoa  7565  ovmpo  7570  frecseq123  8269  oaword1  8554  oneo  8583  oeoalem  8598  oeoelem  8600  nnaword1  8631  nnneo  8656  erov  8810  enrefg  8982  f1imaen  9014  mapxpen  9145  0sdom1dom  9240  acnlem  10045  djucomen  10174  nnadju  10194  infmap  10573  canthnumlem  10645  tskin  10756  tsksn  10757  tsk0  10760  gruxp  10804  gruina  10815  genpprecl  10998  addsrpr  11072  mulsrpr  11073  supsrlem  11108  mulrid  11216  00id  11393  mul02lem1  11394  ltneg  11718  leneg  11721  suble0  11732  div1  11907  nnaddcl  12239  nnmulcl  12240  nnge1  12244  nnsub  12260  2halves  12444  halfaddsub  12449  addltmul  12452  fcdmnn0fsuppg  12535  zleltp1  12617  nnaddm1cl  12623  zextlt  12640  eluzp1p1  12854  uzaddcl  12892  znq  12940  xrre  13152  xrre2  13153  fzshftral  13593  fraclt1  13771  expadd  14074  expmul  14077  sqmul  14088  expubnd  14146  bernneq  14196  faclbnd2  14255  faclbnd6  14263  hashgadd  14341  hashun2  14347  hashunsnggt  14358  hashssdif  14376  hashfun  14401  ccatlcan  14672  ccatrcan  14673  pfx2  14902  shftval3  15027  01sqrexlem1  15193  caubnd2  15308  bpoly2  16005  bpoly3  16006  fsumcube  16008  efexp  16048  efival  16099  cos01gt0  16138  odd2np1  16288  halfleoddlt  16309  omoe  16311  opeo  16312  divalglem5  16344  sqgcd  16506  nn0seqcvgd  16511  prmdvdssq  16659  phiprmpw  16713  eulerthlem2  16719  odzcllem  16729  pythagtriplem15  16766  pythagtriplem17  16768  pcelnn  16807  4sqlem3  16887  fullfunc  17861  fthfunc  17862  prfcl  18159  curf1cl  18185  curfcl  18189  hofcl  18216  odinv  19470  lsmelvalix  19550  dprdval  19914  lsp0  20764  lss0v  20771  zndvds0  21325  frlmlbs  21571  lindfres  21597  lmisfree  21616  coe1scl  22029  ntrin  22785  lpsscls  22865  restperf  22908  txuni2  23289  txopn  23326  elqtop2  23425  xkocnv  23538  ptcmp  23782  xblpnfps  24121  xblpnf  24122  bl2in  24126  unirnblps  24145  unirnbl  24146  blpnfctr  24162  dscopn  24302  bcthlem4  25075  minveclem2  25174  minveclem4  25180  icombl  25313  i1fadd  25444  i1fmul  25445  dvn1  25676  dvexp3  25730  plyconst  25955  plyid  25958  sincosq1eq  26258  sinord  26279  cxpp1  26424  cxpsqrtlem  26446  cxpsqrt  26447  angneg  26544  dcubic  26587  issqf  26876  ppiub  26943  bposlem1  27023  bposlem2  27024  bposlem9  27031  nosupno  27442  nosupfv  27445  noinfno  27457  noinffv  27460  scutval  27538  scutun12  27548  cuteq0  27570  cuteq1  27571  cofcut1  27645  cofcutr  27649  addscut2  27701  sleadd1  27711  addsuniflem  27723  addsasslem1  27725  addsasslem2  27726  negscut2  27753  mulsproplem12  27822  mulscut2  27828  divs1  27890  precsexlem10  27901  precsexlem11  27902  axlowdimlem6  28472  axlowdimlem14  28480  axcontlem2  28490  pthdlem2  29292  0ewlk  29634  ipasslem1  30351  ipasslem2  30352  ipasslem11  30360  minvecolem2  30395  minvecolem3  30396  minvecolem4  30400  shsva  30840  h1datomi  31101  lnfnmuli  31564  leopsq  31649  nmopleid  31659  opsqrlem6  31665  pjnmopi  31668  hstle  31750  csmdsymi  31854  atcvatlem  31905  dpfrac1  32325  cshf1o  32393  cycpmconjslem2  32584  rspidlid  32761  elsx  33490  dya2iocnrect  33578  cvmliftphtlem  34606  satfv1  34652  satffunlem1lem2  34692  satffunlem1  34696  wlimeq12  35095  fvray  35417  fvline  35420  tailfb  35565  uncov  36772  tan2h  36783  matunitlindflem1  36787  matunitlindflem2  36788  poimirlem32  36823  mblfinlem4  36831  mbfresfi  36837  mbfposadd  36838  itg2addnc  36845  ftc1anclem5  36868  ftc1anclem8  36871  dvasin  36875  heiborlem7  36988  igenidl  37234  el3v3  37392  atlatmstc  38492  dihglblem2N  40468  2xp3dxp2ge1d  41328  factwoffsmonot  41329  eldioph4b  41851  diophren  41853  rmxp1  41973  rmyp1  41974  rmxm1  41975  rmym1  41976  dig0  47379  i0oii  47639  onetansqsecsq  47893  cotsqcscsq  47894