Theorem mp2and 712

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 708	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
5	1, 4	mpd 16	1 ⊢ (𝜑 → 𝜃)

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

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

This theorem is used by:  reu2eqd  3697  ssnelpssd  4067  sotrd  5593  frpomin  6342  fvf1pr  7311  tfisi  7858  tfindsg2  7861  mposn  8103  frxp2  8145  smoord  8357  oelimcl  8591  oeeui  8593  nnawordex  8628  omabs  8642  naddssim  8677  naddel12  8692  ertrd  8716  en2prd  9057  omxpenlem  9079  fodomfir  9300  ixpfi2  9320  supssd  9436  infssd  9467  oismo  9515  cantnflem1c  9669  cantnflem1  9671  cantnflem3  9673  infxpenc2  10028  isfin2-2  10324  axdc2lem  10453  r1limwun  10748  letrd  11394  lelttrd  11395  ltletrd  11397  lttrd  11398  le2subd  11861  ltleaddd  11862  leltaddd  11863  lt2subd  11865  ltmul12a  12098  lemul12ad  12184  lemul12bd  12185  lt2halvesd  12519  0nn0m1nnn0  12678  uzind  12716  uztrn  12908  xrlttrd  13212  xrlelttrd  13213  xrltletrd  13214  xrletrd  13215  supxrunb1  13373  supxrunb2  13374  ixxun  13416  ixxss1  13418  ixxss2  13419  ixxss12  13420  fldiv4p1lem1div2  13898  fldiv4lem1div2uz2  13899  seqf1o  14109  faclbnd3  14358  relexpindlem  15138  01sqrexlem1  15331  01sqrexlem4  15334  01sqrexlem7  15337  abs3lemd  15553  rlimcn3  15679  o1of2  15702  lo1add  15716  lo1mul  15717  modfsummod  15883  mertenslem1  15975  sin01gt0  16282  cos01gt0  16283  sin02gt0  16284  dvds2addd  16386  dvds2subd  16387  dvdstrd  16389  bezoutlem4  16636  mulgcd  16642  lcmgcdeq  16706  mulgcddvds  16749  rpmulgcd2  16750  rpdvds  16754  divgcdcoprmex  16760  phimullem  16874  eulerthlem1  16876  eulerthlem2  16877  prmdiveq  16881  pythagtriplem4  16915  pcqmul  16949  pcgcd1  16973  pcadd  16985  pockthlem  17001  prmreclem2  17013  4sqlem16  17056  ramub1lem1  17122  ramub1lem2  17123  prmgaplem7  17153  iscatd2  17773  cicsym  17897  initoeu2  18109  joinval  18467  meetval  18481  lattrd  18538  latledi  18569  mulgass  19235  gaorber  19436  psgnunilem4  19625  efgredlem  19875  odadd2  19977  dmdprdpr  20179  ablfacrp2  20197  ablfac1b  20200  ablfac1eu  20203  pgpfac1  20210  orngmul  21032  ssdifidlprm  21550  gsumbagdiaglem  22147  mdetunilem1  22835  mdetunilem4  22838  mdetunilem9  22843  neiptoptop  23357  lmcnp  23530  txcls  23831  txlly  23863  txnlly  23864  tx1stc  23877  alexsubALTlem1  24274  prdsmet  24597  blin2  24656  blcvx  25025  tgqioo  25027  metnrmlem3  25089  iscmet3lem2  25521  ovolmge0  25706  ovolunlem2  25727  mbfi1flimlem  25951  mbfmullem  25954  itg2add  25988  dvferm1lem  26213  dvferm2lem  26215  dvlip2  26224  dvge0  26235  dvcvx  26249  dvfsumabs  26252  ftc1a  26266  plyadd  26444  plymul  26445  dgrlb  26463  plydivlem4  26527  vieta1lem2  26542  ulmdvlem3  26635  sinq12gt0  26742  logdivlti  26855  fsumharmonic  27246  mpodvdsmulf1o  27428  dvdsmulf1o  27430  logfacubnd  27455  perfectlem1  27463  dchrptlem2  27499  2sqlem5  27656  2sqlem8  27660  2sqmod  27670  dchrisum0flblem2  27743  pntibndlem2  27825  pntlemr  27836  pntlemp  27844  nosupbnd1  27948  nosupbnd2lem1  27949  nosupbnd2  27950  noinfbnd1  27963  noinfbnd2lem1  27964  noinfbnd2  27965  noetasuplem4  27970  noetainflem4  27974  ltstrd  27997  ltlestrd  27998  leltstrd  27999  lestrd  28000  oldbdayim  28152  mulsproplem5  28383  mulsproplem6  28384  mulsproplem7  28385  mulsproplem8  28386  ltmulsd  28400  bdayfinbndlem1  28730  bdayfinbnd  28732  axtgpasch  28806  tgjustr  28813  wlkcompim  30077  wwlksnredwwlkn  30349  wwlksnextsurj  30354  upgr4cycl4dv4e  30651  ex-natded5.2-2  30871  chscllem2  32105  chscllem4  32107  nmopge0  32378  nmfnge0  32394  nmoptrii  32561  staddi  32713  stadd3i  32715  atcvatlem  32852  xrofsup  33225  xrge0addgt0  33444  archiabllem2c  33622  linds2eq  33801  lbsdiflsp0  34123  fedgmullem2  34127  esumpmono  34576  unelldsys  34656  omssubaddlem  34797  signstfvneq0  35067  axtgupdim2ALTV  35163  bnj1098  35280  bnj1110  35478  bnj1121  35481  cplgredgex  35706  erdszelem8  35764  txsconn  35807  cvmlift2lem10  35878  cvmlift3lem7  35891  dfon2lem6  36352  dfon2lem8  36354  cgrtr4d  36552  cgrtrand  36560  cgrtr3and  36562  cgrextendand  36576  btwnexch3and  36588  btwnexchand  36593  linecgrand  36649  endofsegidand  36653  btwnconn1lem4  36657  btwnconn1lem8  36661  btwnconn1lem11  36664  btwnconn1lem12  36665  brsegle2  36676  seglecgr12im  36677  segleantisym  36682  colinbtwnle  36685  broutsideof2  36689  outsideoftr  36696  outsidele  36699  lineelsb2  36715  linethru  36720  ontr2d  36767  ltnadd  36785  gtinf  36925  weiunpo  37071  copsex2d  37878  relowlssretop  38104  pibt2  38158  heicant  38391  mbfresfi  38402  ftc1anclem6  38434  eqvreltrd  39427  riotasv2d  39817  lcvnbtwn2  39887  lcvnbtwn3  39888  lcvexchlem4  39897  omlfh1N  40118  atlen0  40170  atlatmstc  40179  cvratlem  40281  lnnat  40287  2atlt  40299  athgt  40316  1cvratex  40333  ps-2  40338  llncmp  40382  llncvrlpln  40418  lplncmp  40422  lplncvrlvol  40476  lvolcmp  40477  dalemcea  40520  dalem-cly  40531  dalem10  40533  dalem17  40540  dalem25  40558  dalem38  40570  dalem44  40576  dalem55  40587  2atm2atN  40645  cdlema1N  40651  paddasslem5  40684  dalawlem3  40733  dalawlem7  40737  dalawlem11  40741  dalawlem12  40742  lhp0lt  40863  4atexlemc  40929  cdlemg33a  41566  cdlemg33  41571  cdlemk51  41813  dia2dimlem2  41925  dia2dimlem3  41926  dihmeetlem20N  42186  coprmdvds2d  42854  flt4lem2  43480  flt4lem5f  43490  ismrcd2  43531  pellqrex  43707  jm2.17b  43789  jm2.26lem3  43829  fnwe2lem2  43879  omabs2  44160  addrcom  45284  infxrunb2  46184  0ellimcdiv  46464  dvnprodlem1  46761  stoweidlem15  46830  stoweidlem26  46841  stoweidlem28  46843  stoweidlem32  46847  stoweidlem44  46859  meadjuni  47272  dfatcolem  48130  icceuelpart  48323  perfectALTVlem1  48624  bgoldbtbndlem2  48709  bgoldbtbndlem3  48710  copisnmnd  49071  assintopass  49116  lcoss  49353  islindeps2  49400  isldepslvec2  49402  isisod  49940  euendfunc  50439