Theorem mp3an3 1479

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an13  1481  mp3an23  1482  mp3anl3  1486  el3v3  3459  opelxp  5684  ov  7553  ovmpoa  7564  ovmpo  7569  frecseq123  8279  oaword1  8539  oneo  8568  oeoalem  8584  oeoelem  8586  nnaword1  8617  nnneo  8643  erov  8814  uncov  8872  enrefg  8990  f1imaen  9023  mapxpen  9141  0sdom1dom  9216  acnlem  10084  djucomen  10213  nnadju  10233  infmap  10618  canthnumlem  10690  tskin  10801  tsksn  10802  tsk0  10805  gruxp  10849  gruina  10860  genpprecl  11043  addsrpr  11117  mulsrpr  11118  supsrlem  11153  mulrid  11263  00id  11442  mul02lem1  11443  ltneg  11771  leneg  11774  suble0  11785  div1  11961  nnaddcl  12313  nnmulcl  12314  nnge1  12321  nnsub  12337  2halves  12519  halfaddsub  12534  addltmul  12537  fcdmnn0fsuppg  12621  zleltp1  12702  nnaddm1cl  12711  zextlt  12728  eluzp1p1  12948  uzaddcl  12986  znq  13034  xrre  13254  xrre2  13255  fzshftral  13703  fraclt1  13896  expadd  14201  expmul  14204  sqmul  14216  expubnd  14275  bernneq  14326  faclbnd2  14388  faclbnd6  14396  hashgadd  14474  hashun2  14480  hashunsnggt  14491  hashssdif  14510  hashfun  14535  ccatlcan  14820  ccatrcan  14821  pfx2  15051  shftval3  15182  01sqrexlem1  15362  caubnd2  15478  bpoly2  16176  bpoly3  16177  fsumcube  16179  efexp  16222  efival  16273  cos01gt0  16312  odd2np1  16464  halfleoddlt  16485  omoe  16487  opeo  16488  divalglem5  16520  sqgcd  16685  nn0seqcvgd  16693  prmdvdssq  16842  phiprmpw  16900  eulerthlem2  16906  odzcllem  16917  pythagtriplem15  16954  pythagtriplem17  16956  pcelnn  16995  4sqlem3  17075  fullfunc  18030  fthfunc  18031  prfcl  18324  curf1cl  18349  curfcl  18353  hofcl  18380  odinv  19722  lsmelvalix  19802  dprdval  20166  lsp0  21231  lss0v  21238  zndvds0  21803  frlmlbs  22050  lindfres  22076  lmisfree  22095  coe1scl  22553  matunitlindflem1  22941  matunitlindflem2  22942  ntrin  23326  lpsscls  23406  restperf  23449  txuni2  23831  txopn  23868  elqtop2  23967  xkocnv  24080  ptcmp  24324  xblpnfps  24661  xblpnf  24662  bl2in  24666  unirnblps  24685  unirnbl  24686  blpnfctr  24702  dscopn  24839  bcthlem4  25595  minveclem2  25694  minveclem4  25700  icombl  25832  i1fadd  25963  i1fmul  25964  dvn1  26193  dvexp3  26245  plyconst  26471  plyid  26474  sincosq1eq  26790  sinord  26811  cxpp1  26957  cxpsqrtlem  26979  cxpsqrt  26980  angneg  27080  dcubic  27123  issqf  27412  ppiub  27480  bposlem1  27560  bposlem2  27561  bposlem9  27568  nosupno  27979  nosupfv  27982  noinfno  27994  noinffv  27997  cutsval  28085  cutsun12  28095  cuteq0  28120  cuteq1  28122  cofcut1  28225  cofcutr  28229  addcuts2  28284  leadds1  28294  addsuniflem  28306  addsasslem1  28308  addsasslem2  28309  negcut2  28345  mulsproplem12  28432  mulcut2  28438  divs1  28509  precsexlem10  28521  precsexlem11  28522  bdayons  28581  n0s0suc  28647  nnzsubs  28690  zmulscld  28702  elz12si  28778  axlowdimlem6  29444  axlowdimlem14  29452  axcontlem2  29462  pthdlem2  30273  0ewlk  30624  ipasslem1  31352  ipasslem2  31353  ipasslem11  31361  minvecolem2  31396  minvecolem3  31397  minvecolem4  31401  shsva  31841  h1datomi  32102  lnfnmuli  32565  leopsq  32650  nmopleid  32660  opsqrlem6  32666  pjnmopi  32669  hstle  32751  csmdsymi  32855  atcvatlem  32906  dpfrac1  33377  cshf1o  33442  rspidlid  33849  elsx  34746  dya2iocnrect  34833  r1omhf  35655  cvmliftphtlem  35997  satfv1  36043  satffunlem1lem2  36083  satffunlem1  36087  wlimeq12  36497  fvray  36822  fvline  36825  tailfb  37081  ttc0elw  37231  tan2h  38449  poimirlem32  38484  mblfinlem4  38492  mbfresfi  38498  mbfposadd  38499  itg2addnc  38506  ftc1anclem5  38529  ftc1anclem8  38532  dvasin  38536  heiborlem7  38665  igenidl  38911  atlatmstc  40290  dihglblem2N  42265  eldioph4b  43750  diophren  43752  rmxp1  43871  rmyp1  43872  rmxm1  43873  rmym1  43874  dfgric2  48929  gpgov  49056  dig0  49634  i0oii  49944  iinfconstbas  50090  onetansqsecsq  50770  cotsqcscsq  50771