Theorem mp2and 700

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mp2and.1	⊢ (𝜑 → 𝜓)
mp2and.2	⊢ (𝜑 → 𝜒)
mp2and.3	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mp2and	⊢ (𝜑 → 𝜃)

Proof of Theorem mp2and

Step	Hyp	Ref	Expression
1		mp2and.2	. 2 ⊢ (𝜑 → 𝜒)
2		mp2and.1	. . 3 ⊢ (𝜑 → 𝜓)
3		mp2and.3	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
4	2, 3	mpand 696	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  reu2eqd  3695  ssnelpssd  4068  sotrd  5559  frpomin  6299  fvf1pr  7255  tfisi  7803  tfindsg2  7806  mposn  8047  frxp2  8088  smoord  8299  oelimcl  8530  oeeui  8532  nnawordex  8567  omabs  8581  naddssim  8615  naddel12  8630  ertrd  8654  en2prd  8988  omxpenlem  9010  fodomfir  9232  ixpfi2  9254  supssd  9370  infssd  9401  oismo  9449  cantnflem1c  9600  cantnflem1  9602  cantnflem3  9604  infxpenc2  9936  isfin2-2  10233  axdc2lem  10362  r1limwun  10651  letrd  11294  lelttrd  11295  ltletrd  11297  lttrd  11298  le2subd  11761  ltleaddd  11762  leltaddd  11763  lt2subd  11765  ltmul12a  12001  lemul12ad  12088  lemul12bd  12089  lt2halvesd  12393  uzind  12588  uztrn  12773  xrlttrd  13077  xrlelttrd  13078  xrltletrd  13079  xrletrd  13080  supxrunb1  13238  supxrunb2  13239  ixxun  13281  ixxss1  13283  ixxss2  13284  ixxss12  13285  fldiv4p1lem1div2  13759  fldiv4lem1div2uz2  13760  seqf1o  13970  faclbnd3  14219  relexpindlem  14990  01sqrexlem1  15169  01sqrexlem4  15172  01sqrexlem7  15175  abs3lemd  15391  rlimcn3  15517  o1of2  15540  lo1add  15554  lo1mul  15555  modfsummod  15721  mertenslem1  15811  sin01gt0  16119  cos01gt0  16120  sin02gt0  16121  dvds2addd  16223  dvds2subd  16224  dvdstrd  16226  bezoutlem4  16473  mulgcd  16479  lcmgcdeq  16543  mulgcddvds  16586  rpmulgcd2  16587  rpdvds  16591  divgcdcoprmex  16597  phimullem  16710  eulerthlem1  16712  eulerthlem2  16713  prmdiveq  16717  pythagtriplem4  16751  pcqmul  16785  pcgcd1  16809  pcadd  16821  pockthlem  16837  prmreclem2  16849  4sqlem16  16892  ramub1lem1  16958  ramub1lem2  16959  prmgaplem7  16989  iscatd2  17608  cicsym  17732  initoeu2  17944  joinval  18302  meetval  18316  lattrd  18373  latledi  18404  mulgass  19045  gaorber  19241  psgnunilem4  19430  efgredlem  19680  odadd2  19782  dmdprdpr  19984  ablfacrp2  20002  ablfac1b  20005  ablfac1eu  20008  pgpfac1  20015  orngmul  20802  gsumbagdiaglem  21890  mdetunilem1  22560  mdetunilem4  22563  mdetunilem9  22568  neiptoptop  23079  lmcnp  23252  txcls  23552  txlly  23584  txnlly  23585  tx1stc  23598  alexsubALTlem1  23995  prdsmet  24318  blin2  24377  blcvx  24746  tgqioo  24748  metnrmlem3  24810  iscmet3lem2  25252  ovolmge0  25438  ovolunlem2  25459  mbfi1flimlem  25683  mbfmullem  25686  itg2add  25720  dvferm1lem  25948  dvferm2lem  25950  dvlip2  25960  dvge0  25971  dvcvx  25985  dvfsumabs  25989  ftc1a  26004  plyadd  26182  plymul  26183  dgrlb  26201  plydivlem4  26264  vieta1lem2  26279  ulmdvlem3  26371  sinq12gt0  26476  logdivlti  26589  fsumharmonic  26982  mpodvdsmulf1o  27164  dvdsmulf1o  27166  logfacubnd  27192  perfectlem1  27200  dchrptlem2  27236  2sqlem5  27393  2sqlem8  27397  2sqmod  27407  dchrisum0flblem2  27480  pntibndlem2  27562  pntlemr  27573  pntlemp  27581  nosupbnd1  27686  nosupbnd2lem1  27687  nosupbnd2  27688  noinfbnd1  27701  noinfbnd2lem1  27702  noinfbnd2  27703  noetasuplem4  27708  noetainflem4  27712  slttrd  27735  sltletrd  27736  slelttrd  27737  sletrd  27738  oldbdayim  27871  mulsproplem5  28102  mulsproplem6  28103  mulsproplem7  28104  mulsproplem8  28105  sltmuld  28119  bdayfinbndlem1  28446  bdayfinbnd  28448  axtgpasch  28522  tgjustr  28529  wlkcompim  29688  wwlksnredwwlkn  29951  wwlksnextsurj  29956  upgr4cycl4dv4e  30243  ex-natded5.2-2  30463  chscllem2  31696  chscllem4  31698  nmopge0  31969  nmfnge0  31985  nmoptrii  32152  staddi  32304  stadd3i  32306  atcvatlem  32443  xrofsup  32828  xrge0addgt0  33080  archiabllem2c  33258  linds2eq  33443  ssdifidlprm  33520  lbsdiflsp0  33764  fedgmullem2  33768  esumpmono  34217  unelldsys  34296  omssubaddlem  34437  signstfvneq0  34710  axtgupdim2ALTV  34806  bnj1098  34920  bnj1110  35119  bnj1121  35122  0nn0m1nnn0  35288  cplgredgex  35296  erdszelem8  35373  txsconn  35416  cvmlift2lem10  35487  cvmlift3lem7  35500  dfon2lem6  35961  dfon2lem8  35963  cgrtr4d  36160  cgrtrand  36168  cgrtr3and  36170  cgrextendand  36184  btwnexch3and  36196  btwnexchand  36201  linecgrand  36257  endofsegidand  36261  btwnconn1lem4  36265  btwnconn1lem8  36269  btwnconn1lem11  36272  btwnconn1lem12  36273  brsegle2  36284  seglecgr12im  36285  segleantisym  36290  colinbtwnle  36293  broutsideof2  36297  outsideoftr  36304  outsidele  36307  lineelsb2  36323  linethru  36328  gtinf  36494  weiunpo  36640  copsex2d  37315  relowlssretop  37539  pibt2  37593  heicant  37827  mbfresfi  37838  ftc1anclem6  37870  eqvreltrd  38864  riotasv2d  39254  lcvnbtwn2  39324  lcvnbtwn3  39325  lcvexchlem4  39334  omlfh1N  39555  atlen0  39607  atlatmstc  39616  cvratlem  39718  lnnat  39724  2atlt  39736  athgt  39753  1cvratex  39770  ps-2  39775  llncmp  39819  llncvrlpln  39855  lplncmp  39859  lplncvrlvol  39913  lvolcmp  39914  dalemcea  39957  dalem-cly  39968  dalem10  39970  dalem17  39977  dalem25  39995  dalem38  40007  dalem44  40013  dalem55  40024  2atm2atN  40082  cdlema1N  40088  paddasslem5  40121  dalawlem3  40170  dalawlem7  40174  dalawlem11  40178  dalawlem12  40179  lhp0lt  40300  4atexlemc  40366  cdlemg33a  41003  cdlemg33  41008  cdlemk51  41250  dia2dimlem2  41362  dia2dimlem3  41363  dihmeetlem20N  41623  coprmdvds2d  42292  flt4lem2  42926  flt4lem5f  42936  ismrcd2  42977  pellqrex  43157  jm2.17b  43239  jm2.26lem3  43279  fnwe2lem2  43329  omabs2  43610  addrcom  44751  infxrunb2  45648  0ellimcdiv  45929  dvnprodlem1  46226  stoweidlem15  46295  stoweidlem26  46306  stoweidlem28  46308  stoweidlem32  46312  stoweidlem44  46324  meadjuni  46737  natglobalincr  47157  dfatcolem  47537  icceuelpart  47718  perfectALTVlem1  48003  bgoldbtbndlem2  48088  bgoldbtbndlem3  48089  copisnmnd  48451  assintopass  48496  lcoss  48718  islindeps2  48765  isldepslvec2  48767  isisod  49308  euendfunc  49807