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

This theorem is referenced by:  mp3an13  1450  mp3an23  1451  mp3anl3  1455  opelxp  5616  ov  7395  ovmpoa  7406  ovmpo  7411  frecseq123  8069  oaword1  8345  oneo  8374  oeoalem  8389  oeoelem  8391  nnaword1  8422  nnneo  8445  erov  8561  enrefg  8727  f1imaen  8757  mapxpen  8879  acnlem  9735  djucomen  9864  nnadju  9884  infmap  10263  canthnumlem  10335  tskin  10446  tsksn  10447  tsk0  10450  gruxp  10494  gruina  10505  genpprecl  10688  addsrpr  10762  mulsrpr  10763  supsrlem  10798  mulid1  10904  00id  11080  mul02lem1  11081  ltneg  11405  leneg  11408  suble0  11419  div1  11594  nnaddcl  11926  nnmulcl  11927  nnge1  11931  nnsub  11947  2halves  12131  halfaddsub  12136  addltmul  12139  frnnn0fsuppg  12222  zleltp1  12301  nnaddm1cl  12307  zextlt  12324  eluzp1p1  12539  uzaddcl  12573  znq  12621  xrre  12832  xrre2  12833  fzshftral  13273  fraclt1  13450  expadd  13753  expmul  13756  sqmul  13767  expubnd  13823  bernneq  13872  faclbnd2  13933  faclbnd6  13941  hashgadd  14020  hashun2  14026  hashunsnggt  14037  hashssdif  14055  hashfun  14080  ccatlcan  14359  ccatrcan  14360  pfx2  14588  shftval3  14715  sqrlem1  14882  caubnd2  14997  bpoly2  15695  bpoly3  15696  fsumcube  15698  efexp  15738  efival  15789  cos01gt0  15828  odd2np1  15978  halfleoddlt  15999  omoe  16001  opeo  16002  divalglem5  16034  gcdmultipleOLD  16188  sqgcd  16198  nn0seqcvgd  16203  prmdvdssq  16351  phiprmpw  16405  eulerthlem2  16411  odzcllem  16421  pythagtriplem15  16458  pythagtriplem17  16460  pcelnn  16499  4sqlem3  16579  fullfunc  17538  fthfunc  17539  prfcl  17836  curf1cl  17862  curfcl  17866  hofcl  17893  odinv  19083  lsmelvalix  19161  dprdval  19521  lsp0  20186  lss0v  20193  zndvds0  20670  frlmlbs  20914  lindfres  20940  lmisfree  20959  coe1scl  21368  ntrin  22120  lpsscls  22200  restperf  22243  txuni2  22624  txopn  22661  elqtop2  22760  xkocnv  22873  ptcmp  23117  xblpnfps  23456  xblpnf  23457  bl2in  23461  unirnblps  23480  unirnbl  23481  blpnfctr  23497  dscopn  23635  bcthlem4  24396  minveclem2  24495  minveclem4  24501  icombl  24633  i1fadd  24764  i1fmul  24765  dvn1  24995  dvexp3  25047  plyconst  25272  plyid  25275  sincosq1eq  25574  sinord  25595  cxpp1  25740  cxpsqrtlem  25762  cxpsqrt  25763  angneg  25858  dcubic  25901  issqf  26190  ppiub  26257  bposlem1  26337  bposlem2  26338  bposlem9  26345  axlowdimlem6  27218  axlowdimlem14  27226  axcontlem2  27236  pthdlem2  28037  0ewlk  28379  ipasslem1  29094  ipasslem2  29095  ipasslem11  29103  minvecolem2  29138  minvecolem3  29139  minvecolem4  29143  shsva  29583  h1datomi  29844  lnfnmuli  30307  leopsq  30392  nmopleid  30402  opsqrlem6  30408  pjnmopi  30411  hstle  30493  csmdsymi  30597  atcvatlem  30648  dpfrac1  31068  cshf1o  31136  cycpmconjslem2  31324  rspidlid  31472  elsx  32062  dya2iocnrect  32148  cvmliftphtlem  33179  satfv1  33225  satffunlem1lem2  33265  satffunlem1  33269  wlimeq12  33740  nosupno  33833  nosupfv  33836  noinfno  33848  noinffv  33851  scutval  33921  scutun12  33931  cofcut1  34017  cofcutr  34019  fvray  34370  fvline  34373  tailfb  34493  uncov  35685  tan2h  35696  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem32  35736  mblfinlem4  35744  mbfresfi  35750  mbfposadd  35751  itg2addnc  35758  ftc1anclem5  35781  ftc1anclem8  35784  dvasin  35788  heiborlem7  35902  igenidl  36148  el3v3  36301  atlatmstc  37260  dihglblem2N  39235  2xp3dxp2ge1d  40090  factwoffsmonot  40091  eldioph4b  40549  diophren  40551  rmxp1  40670  rmyp1  40671  rmxm1  40672  rmym1  40673  dig0  45840  i0oii  46101  onetansqsecsq  46349  cotsqcscsq  46350