Theorem mp3an3 1453

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

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

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 1089

This theorem is referenced by:  mp3an13  1455  mp3an23  1456  mp3anl3  1460  el3v3  3439  opelxp  5664  ov  7508  ovmpoa  7519  ovmpo  7524  frecseq123  8229  oaword1  8484  oneo  8513  oeoalem  8529  oeoelem  8531  nnaword1  8562  nnneo  8588  erov  8758  enrefg  8928  f1imaen  8961  mapxpen  9078  0sdom1dom  9153  acnlem  9967  djucomen  10097  nnadju  10117  infmap  10496  canthnumlem  10568  tskin  10679  tsksn  10680  tsk0  10683  gruxp  10727  gruina  10738  genpprecl  10921  addsrpr  10995  mulsrpr  10996  supsrlem  11031  mulrid  11139  00id  11318  mul02lem1  11319  ltneg  11647  leneg  11650  suble0  11661  div1  11841  nnaddcl  12194  nnmulcl  12195  nnge1  12202  nnsub  12218  2halves  12392  halfaddsub  12407  addltmul  12410  fcdmnn0fsuppg  12494  zleltp1  12575  nnaddm1cl  12583  zextlt  12600  eluzp1p1  12813  uzaddcl  12851  znq  12899  xrre  13118  xrre2  13119  fzshftral  13566  fraclt1  13758  expadd  14063  expmul  14066  sqmul  14078  expubnd  14137  bernneq  14188  faclbnd2  14250  faclbnd6  14258  hashgadd  14336  hashun2  14342  hashunsnggt  14353  hashssdif  14371  hashfun  14396  ccatlcan  14677  ccatrcan  14678  pfx2  14906  shftval3  15035  01sqrexlem1  15201  caubnd2  15317  bpoly2  16019  bpoly3  16020  fsumcube  16022  efexp  16065  efival  16116  cos01gt0  16155  odd2np1  16307  halfleoddlt  16328  omoe  16330  opeo  16331  divalglem5  16363  sqgcd  16528  nn0seqcvgd  16536  prmdvdssq  16685  phiprmpw  16743  eulerthlem2  16749  odzcllem  16760  pythagtriplem15  16797  pythagtriplem17  16799  pcelnn  16838  4sqlem3  16918  fullfunc  17872  fthfunc  17873  prfcl  18166  curf1cl  18191  curfcl  18195  hofcl  18222  odinv  19533  lsmelvalix  19613  dprdval  19977  lsp0  21001  lss0v  21009  zndvds0  21546  frlmlbs  21793  lindfres  21819  lmisfree  21838  coe1scl  22268  ntrin  23042  lpsscls  23122  restperf  23165  txuni2  23546  txopn  23583  elqtop2  23682  xkocnv  23795  ptcmp  24039  xblpnfps  24376  xblpnf  24377  bl2in  24381  unirnblps  24400  unirnbl  24401  blpnfctr  24417  dscopn  24554  bcthlem4  25310  minveclem2  25409  minveclem4  25415  icombl  25547  i1fadd  25678  i1fmul  25679  dvn1  25909  dvexp3  25961  plyconst  26187  plyid  26190  sincosq1eq  26495  sinord  26517  cxpp1  26663  cxpsqrtlem  26685  cxpsqrt  26686  angneg  26786  dcubic  26829  issqf  27119  ppiub  27187  bposlem1  27267  bposlem2  27268  bposlem9  27275  nosupno  27687  nosupfv  27690  noinfno  27702  noinffv  27705  cutsval  27792  cutsun12  27802  cuteq0  27827  cuteq1  27829  cofcut1  27932  cofcutr  27936  addcuts2  27991  leadds1  28001  addsuniflem  28013  addsasslem1  28015  addsasslem2  28016  negcut2  28052  mulsproplem12  28139  mulcut2  28145  divs1  28216  precsexlem10  28228  precsexlem11  28229  bdayons  28288  n0s0suc  28354  nnzsubs  28397  zmulscld  28409  elz12si  28485  axlowdimlem6  29036  axlowdimlem14  29044  axcontlem2  29054  pthdlem2  29857  0ewlk  30205  ipasslem1  30923  ipasslem2  30924  ipasslem11  30932  minvecolem2  30967  minvecolem3  30968  minvecolem4  30972  shsva  31412  h1datomi  31673  lnfnmuli  32136  leopsq  32221  nmopleid  32231  opsqrlem6  32237  pjnmopi  32240  hstle  32322  csmdsymi  32426  atcvatlem  32477  dpfrac1  32972  cshf1o  33043  cycpmconjslem2  33237  rspidlid  33456  elsx  34360  dya2iocnrect  34447  r1omhf  35271  cvmliftphtlem  35521  satfv1  35567  satffunlem1lem2  35607  satffunlem1  35611  wlimeq12  36021  fvray  36345  fvline  36348  tailfb  36581  ttc0elw  36731  uncov  37944  tan2h  37955  matunitlindflem1  37959  matunitlindflem2  37960  poimirlem32  37995  mblfinlem4  38003  mbfresfi  38009  mbfposadd  38010  itg2addnc  38017  ftc1anclem5  38040  ftc1anclem8  38043  dvasin  38047  heiborlem7  38160  igenidl  38406  atlatmstc  39787  dihglblem2N  41762  eldioph4b  43265  diophren  43267  rmxp1  43386  rmyp1  43387  rmxm1  43388  rmym1  43389  dfgric2  48411  gpgov  48538  dig0  49102  i0oii  49415  iinfconstbas  49561  onetansqsecsq  50256  cotsqcscsq  50257