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  4046  sotrd  5589  frpomin  6361  fvf1pr  7338  tfisi  7894  tfindsg2  7897  mposn  8141  fnwe2lem3  8174  frxp2  8188  smoord  8401  oelimcl  8637  oeeui  8639  nnawordex  8674  omabs  8688  naddssim  8723  naddel12  8738  ertrd  8762  en2prd  9103  omxpenlem  9125  fodomfir  9347  ixpfi2  9367  supssd  9482  infssd  9513  oismo  9561  cantnflem1c  9715  cantnflem1  9717  cantnflem3  9719  infxpenc2  10128  isfin2-2  10424  axdc2lem  10553  r1limwun  10848  letrd  11494  lelttrd  11495  ltletrd  11497  lttrd  11498  le2subd  11963  ltleaddd  11964  leltaddd  11965  lt2subd  11967  ltmul12a  12200  lemul12ad  12286  lemul12bd  12287  lt2halvesd  12621  0nn0m1nnn0  12780  uzind  12818  uztrn  13010  xrlttrd  13315  xrlelttrd  13316  xrltletrd  13317  xrletrd  13318  supxrunb1  13476  supxrunb2  13477  ixxun  13519  ixxss1  13521  ixxss2  13522  ixxss12  13523  fldiv4p1lem1div2  14002  fldiv4lem1div2uz2  14003  seqf1o  14213  faclbnd3  14463  relexpindlem  15245  01sqrexlem1  15438  01sqrexlem4  15441  01sqrexlem7  15444  abs3lemd  15660  rlimcn3  15786  o1of2  15809  lo1add  15823  lo1mul  15824  modfsummod  15990  mertenslem1  16082  sin01gt0  16387  cos01gt0  16388  sin02gt0  16389  dvds2addd  16491  dvds2subd  16492  dvdstrd  16494  bezoutlem4  16744  mulgcd  16750  lcmgcdeq  16816  mulgcddvds  16859  rpmulgcd2  16860  rpdvds  16864  divgcdcoprmex  16870  phimullem  16985  eulerthlem1  16987  eulerthlem2  16988  prmdiveq  16992  pythagtriplem4  17026  pcqmul  17060  pcgcd1  17084  pcadd  17096  pockthlem  17112  prmreclem2  17124  4sqlem16  17167  ramub1lem1  17233  ramub1lem2  17234  prmgaplem7  17264  iscatd2  17884  cicsym  18008  initoeu2  18220  joinval  18578  meetval  18592  lattrd  18649  latledi  18680  mulgass  19350  gaorber  19552  psgnunilem4  19741  efgredlem  19991  odadd2  20093  dmdprdpr  20295  ablfacrp2  20313  ablfac1b  20316  ablfac1eu  20319  pgpfac1  20326  orngmul  21152  ssdifidlprm  21672  gsumbagdiaglem  22269  mdetunilem1  22957  mdetunilem4  22960  mdetunilem9  22965  neiptoptop  23479  lmcnp  23652  txcls  23953  txlly  23985  txnlly  23986  tx1stc  23999  alexsubALTlem1  24396  prdsmet  24719  blin2  24778  blcvx  25147  tgqioo  25149  metnrmlem3  25211  iscmet3lem2  25643  ovolmge0  25828  ovolunlem2  25849  mbfi1flimlem  26073  mbfmullem  26076  itg2add  26110  dvferm1lem  26334  dvferm2lem  26336  dvlip2  26345  dvge0  26356  dvcvx  26370  dvfsumabs  26373  ftc1a  26387  plyadd  26566  plymul  26567  dgrlb  26585  plydivlem4  26647  vieta1lem2  26664  ulmdvlem3  26759  sinq12gt0  26866  logdivlti  26978  fsumharmonic  27369  mpodvdsmulf1o  27551  dvdsmulf1o  27553  logfacubnd  27578  perfectlem1  27586  dchrptlem2  27622  2sqlem5  27779  2sqlem8  27783  2sqmod  27793  dchrisum0flblem2  27866  pntibndlem2  27948  pntlemr  27959  pntlemp  27967  flt4lem5f  28017  nosupbnd1  28101  nosupbnd2lem1  28102  nosupbnd2  28103  noinfbnd1  28116  noinfbnd2lem1  28117  noinfbnd2  28118  noetasuplem4  28123  noetainflem4  28127  ltstrd  28150  ltlestrd  28151  leltstrd  28152  lestrd  28153  oldbdayim  28305  mulsproplem5  28536  mulsproplem6  28537  mulsproplem7  28538  mulsproplem8  28539  ltmulsd  28553  bdayfinbndlem1  28883  bdayfinbnd  28885  axtgpasch  28959  tgjustr  28966  wlkcompim  30242  wwlksnredwwlkn  30514  wwlksnextsurj  30519  upgr4cycl4dv4e  30816  ex-natded5.2-2  31036  chscllem2  32270  chscllem4  32272  nmopge0  32543  nmfnge0  32559  nmoptrii  32726  staddi  32878  stadd3i  32880  atcvatlem  33017  xrofsup  33429  xrge0addgt0  33648  archiabllem2c  33826  linds2eq  34006  lbsdiflsp0  34328  fedgmullem2  34332  esumpmono  34781  unelldsys  34861  omssubaddlem  35001  signstfvneq0  35271  axtgupdim2ALTV  35367  bnj1098  35484  bnj1110  35682  bnj1121  35685  cplgredgex  36062  erdszelem8  36130  txsconn  36173  cvmlift2lem10  36244  cvmlift3lem7  36257  dfon2lem6  36728  dfon2lem8  36730  cgrtr4d  36928  cgrtrand  36936  cgrtr3and  36938  cgrextendand  36952  btwnexch3and  36964  btwnexchand  36969  linecgrand  37025  endofsegidand  37029  btwnconn1lem4  37033  btwnconn1lem8  37037  btwnconn1lem11  37040  btwnconn1lem12  37041  brsegle2  37052  seglecgr12im  37053  segleantisym  37058  colinbtwnle  37061  broutsideof2  37065  outsideoftr  37072  outsidele  37075  lineelsb2  37091  linethru  37096  ontr2d  37127  ltnadd  37145  gtinf  37285  weiunpo  37431  copsex2d  38252  relowlssretop  38478  pibt2  38532  heicant  38765  mbfresfi  38776  ftc1anclem6  38808  eqvreltrd  39816  riotasv2d  40206  lcvnbtwn2  40276  lcvnbtwn3  40277  lcvexchlem4  40286  omlfh1N  40507  atlen0  40559  atlatmstc  40568  cvratlem  40670  lnnat  40676  2atlt  40688  athgt  40705  1cvratex  40722  ps-2  40727  llncmp  40771  llncvrlpln  40807  lplncmp  40811  lplncvrlvol  40865  lvolcmp  40866  dalemcea  40909  dalem-cly  40920  dalem10  40922  dalem17  40929  dalem25  40947  dalem38  40959  dalem44  40965  dalem55  40976  2atm2atN  41034  cdlema1N  41040  paddasslem5  41073  dalawlem3  41122  dalawlem7  41126  dalawlem11  41130  dalawlem12  41131  lhp0lt  41252  4atexlemc  41318  cdlemg33a  41955  cdlemg33  41960  cdlemk51  42202  dia2dimlem2  42314  dia2dimlem3  42315  dihmeetlem20N  42575  coprmdvds2d  43243  ismrcd2  43903  pellqrex  44079  jm2.17b  44161  jm2.26lem3  44201  omabs2  44526  addrcom  45648  infxrunb2  46584  0ellimcdiv  46864  dvnprodlem1  47161  stoweidlem15  47230  stoweidlem26  47241  stoweidlem28  47243  stoweidlem32  47247  stoweidlem44  47259  meadjuni  47672  dfatcolem  48530  icceuelpart  48723  perfectALTVlem1  49024  bgoldbtbndlem2  49109  bgoldbtbndlem3  49110  copisnmnd  49471  assintopass  49516  lcoss  49753  islindeps2  49800  isldepslvec2  49802  isisod  50346  euendfunc  50866