Theorem mp3an3 1446

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  mp3an13  1448  mp3an23  1449  mp3anl3  1453  opelxp  5590  ov  7293  ovmpoa  7304  ovmpo  7309  oaword1  8177  oneo  8206  oeoalem  8221  oeoelem  8223  nnaword1  8254  nnneo  8277  erov  8393  enrefg  8540  f1imaen  8570  mapxpen  8682  acnlem  9473  djucomen  9602  infmap  9997  canthnumlem  10069  tskin  10180  tsksn  10181  tsk0  10184  gruxp  10228  gruina  10239  genpprecl  10422  addsrpr  10496  mulsrpr  10497  supsrlem  10532  mulid1  10638  00id  10814  mul02lem1  10815  ltneg  11139  leneg  11142  suble0  11153  div1  11328  nnaddcl  11659  nnmulcl  11660  nnge1  11664  nnsub  11680  2halves  11864  halfaddsub  11869  addltmul  11872  zleltp1  12032  nnaddm1cl  12038  zextlt  12055  eluzp1p1  12269  uzaddcl  12303  znq  12351  xrre  12561  xrre2  12562  fzshftral  12994  fraclt1  13171  expadd  13470  expmul  13473  sqmul  13484  expubnd  13540  bernneq  13589  faclbnd2  13650  faclbnd6  13658  hashgadd  13737  hashun2  13743  hashunsnggt  13754  hashssdif  13772  hashfun  13797  ccatlcan  14079  ccatrcan  14080  pfx2  14308  shftval3  14434  sqrlem1  14601  caubnd2  14716  bpoly2  15410  bpoly3  15411  fsumcube  15413  efexp  15453  efival  15504  cos01gt0  15543  odd2np1  15689  halfleoddlt  15710  omoe  15712  opeo  15713  divalglem5  15747  gcdmultipleOLD  15899  sqgcd  15908  nn0seqcvgd  15913  phiprmpw  16112  eulerthlem2  16118  odzcllem  16128  pythagtriplem15  16165  pythagtriplem17  16167  pcelnn  16205  4sqlem3  16285  fullfunc  17175  fthfunc  17176  prfcl  17452  curf1cl  17477  curfcl  17481  hofcl  17508  odinv  18687  lsmelvalix  18765  dprdval  19124  lsp0  19780  lss0v  19787  coe1scl  20454  zndvds0  20696  frlmlbs  20940  lindfres  20966  lmisfree  20985  ntrin  21668  lpsscls  21748  restperf  21791  txuni2  22172  txopn  22209  elqtop2  22308  xkocnv  22421  ptcmp  22665  xblpnfps  23004  xblpnf  23005  bl2in  23009  unirnblps  23028  unirnbl  23029  blpnfctr  23045  dscopn  23182  bcthlem4  23929  minveclem2  24028  minveclem4  24034  icombl  24164  i1fadd  24295  i1fmul  24296  dvn1  24522  dvexp3  24574  plyconst  24795  plyid  24798  sincosq1eq  25097  sinord  25117  cxpp1  25262  cxpsqrtlem  25284  cxpsqrt  25285  angneg  25380  dcubic  25423  issqf  25712  ppiub  25779  bposlem1  25859  bposlem2  25860  bposlem9  25867  axlowdimlem6  26732  axlowdimlem14  26740  axcontlem2  26750  pthdlem2  27548  0ewlk  27892  ipasslem1  28607  ipasslem2  28608  ipasslem11  28616  minvecolem2  28651  minvecolem3  28652  minvecolem4  28656  shsva  29096  h1datomi  29357  lnfnmuli  29820  leopsq  29905  nmopleid  29915  opsqrlem6  29921  pjnmopi  29924  hstle  30006  csmdsymi  30110  atcvatlem  30161  dpfrac1  30568  cshf1o  30636  cycpmconjslem2  30797  elsx  31453  dya2iocnrect  31539  cvmliftphtlem  32564  satfv1  32610  satffunlem1lem2  32650  satffunlem1  32654  wlimeq12  33106  frecseq123  33119  nosupno  33203  nosupfv  33206  scutval  33265  scutun12  33271  fvray  33602  fvline  33605  tailfb  33725  uncov  34872  tan2h  34883  matunitlindflem1  34887  matunitlindflem2  34888  poimirlem32  34923  mblfinlem4  34931  mbfresfi  34937  mbfposadd  34938  itg2addnc  34945  ftc1anclem5  34970  ftc1anclem8  34973  dvasin  34977  heiborlem7  35094  igenidl  35340  el3v3  35493  atlatmstc  36454  dihglblem2N  38429  eldioph4b  39406  diophren  39408  rmxp1  39527  rmyp1  39528  rmxm1  39529  rmym1  39530  wepwso  39641  dig0  44665  onetansqsecsq  44859  cotsqcscsq  44860