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  5686  ov  7564  ovmpoa  7575  ovmpo  7580  frecseq123  8300  oaword1  8560  oneo  8589  oeoalem  8605  oeoelem  8607  nnaword1  8638  nnneo  8664  erov  8835  uncov  8893  enrefg  9011  f1imaen  9044  mapxpen  9162  0sdom1dom  9237  elhf4  9912  acnlem  10127  djucomen  10256  nnadju  10276  infmap  10661  canthnumlem  10733  tskin  10844  tsksn  10845  tsk0  10848  gruxp  10892  gruina  10903  genpprecl  11086  addsrpr  11160  mulsrpr  11161  supsrlem  11196  mulrid  11306  00id  11485  mul02lem1  11486  ltneg  11816  leneg  11819  suble0  11830  div1  12006  nnaddcl  12358  nnmulcl  12359  nnge1  12366  nnsub  12382  2halves  12564  halfaddsub  12579  addltmul  12582  fcdmnn0fsuppg  12666  zleltp1  12747  nnaddm1cl  12756  zextlt  12773  eluzp1p1  12993  uzaddcl  13031  znq  13079  xrre  13299  xrre2  13300  fzshftral  13749  fraclt1  13942  expadd  14247  expmul  14250  sqmul  14262  expubnd  14321  bernneq  14373  faclbnd2  14435  faclbnd6  14443  hashgadd  14521  hashun2  14527  hashunsnggt  14538  hashssdif  14557  hashfun  14582  ccatlcan  14867  ccatrcan  14868  pfx2  15098  shftval3  15229  01sqrexlem1  15409  caubnd2  15525  bpoly2  16223  bpoly3  16224  fsumcube  16226  efexp  16269  efival  16320  cos01gt0  16359  odd2np1  16511  halfleoddlt  16532  omoe  16534  opeo  16535  divalglem5  16567  sqgcd  16736  dvdssqnn  16741  nn0seqcvgd  16745  prmdvdssq  16894  phiprmpw  16953  eulerthlem2  16959  odzcllem  16970  pythagtriplem15  17007  pythagtriplem17  17009  pcelnn  17048  4sqlem3  17128  fullfunc  18083  fthfunc  18084  prfcl  18377  curf1cl  18402  curfcl  18406  hofcl  18433  odinv  19775  lsmelvalix  19855  dprdval  20219  lsp0  21284  lss0v  21291  zndvds0  21856  frlmlbs  22103  lindfres  22129  lmisfree  22148  coe1scl  22606  matunitlindflem1  22994  matunitlindflem2  22995  ntrin  23379  lpsscls  23459  restperf  23502  txuni2  23884  txopn  23921  elqtop2  24020  xkocnv  24133  ptcmp  24377  xblpnfps  24714  xblpnf  24715  bl2in  24719  unirnblps  24738  unirnbl  24739  blpnfctr  24755  dscopn  24892  bcthlem4  25648  minveclem2  25747  minveclem4  25753  icombl  25885  i1fadd  26016  i1fmul  26017  dvn1  26246  dvexp3  26298  plyconst  26524  plyid  26527  sincosq1eq  26841  sinord  26862  cxpp1  27008  cxpsqrtlem  27030  cxpsqrt  27031  angneg  27131  dcubic  27174  issqf  27463  ppiub  27531  bposlem1  27611  bposlem2  27612  bposlem9  27619  nosupno  28060  nosupfv  28063  noinfno  28075  noinffv  28078  cutsval  28166  cutsun12  28176  cuteq0  28201  cuteq1  28203  cofcut1  28306  cofcutr  28310  addcuts2  28365  leadds1  28375  addsuniflem  28387  addsasslem1  28389  addsasslem2  28390  negcut2  28426  mulsproplem12  28513  mulcut2  28519  divs1  28590  precsexlem10  28602  precsexlem11  28603  bdayons  28662  n0s0suc  28728  nnzsubs  28771  zmulscld  28783  elz12si  28859  axlowdimlem6  29525  axlowdimlem14  29533  axcontlem2  29543  pthdlem2  30354  0ewlk  30705  ipasslem1  31433  ipasslem2  31434  ipasslem11  31442  minvecolem2  31477  minvecolem3  31478  minvecolem4  31482  shsva  31922  h1datomi  32183  lnfnmuli  32646  leopsq  32731  nmopleid  32741  opsqrlem6  32747  pjnmopi  32750  hstle  32832  csmdsymi  32936  atcvatlem  32987  dpfrac1  33458  cshf1o  33523  rspidlid  33930  elsx  34827  dya2iocnrect  34913  cvmliftphtlem  36082  satfv1  36128  satffunlem1lem2  36168  satffunlem1  36172  wlimeq12  36581  fvray  36906  fvline  36909  tailfb  37165  ttc0elw  37315  tan2h  38536  poimirlem32  38571  mblfinlem4  38579  mbfresfi  38585  mbfposadd  38586  itg2addnc  38593  ftc1anclem5  38616  ftc1anclem8  38619  dvasin  38623  heiborlem7  38752  igenidl  38998  atlatmstc  40377  dihglblem2N  42352  eldioph4b  43818  diophren  43820  rmxp1  43939  rmyp1  43940  rmxm1  43941  rmym1  43942  dfgric2  49013  gpgov  49140  dig0  49718  i0oii  50028  iinfconstbas  50174  onetansqsecsq  50854  cotsqcscsq  50855