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  3693  ssnelpssd  4043  sotrd  5584  frpomin  6343  fvf1pr  7315  tfisi  7870  tfindsg2  7873  mposn  8114  fnwe2lem3  8147  frxp2  8161  smoord  8373  oelimcl  8609  oeeui  8611  nnawordex  8646  omabs  8660  naddssim  8695  naddel12  8710  ertrd  8734  en2prd  9075  omxpenlem  9097  fodomfir  9319  ixpfi2  9339  supssd  9455  infssd  9486  oismo  9534  cantnflem1c  9688  cantnflem1  9690  cantnflem3  9692  infxpenc2  10101  isfin2-2  10397  axdc2lem  10526  r1limwun  10821  letrd  11467  lelttrd  11468  ltletrd  11470  lttrd  11471  le2subd  11936  ltleaddd  11937  leltaddd  11938  lt2subd  11940  ltmul12a  12173  lemul12ad  12259  lemul12bd  12260  lt2halvesd  12594  0nn0m1nnn0  12753  uzind  12791  uztrn  12983  xrlttrd  13288  xrlelttrd  13289  xrltletrd  13290  xrletrd  13291  supxrunb1  13449  supxrunb2  13450  ixxun  13492  ixxss1  13494  ixxss2  13495  ixxss12  13496  fldiv4p1lem1div2  13975  fldiv4lem1div2uz2  13976  seqf1o  14186  faclbnd3  14436  relexpindlem  15216  01sqrexlem1  15409  01sqrexlem4  15412  01sqrexlem7  15415  abs3lemd  15631  rlimcn3  15757  o1of2  15780  lo1add  15794  lo1mul  15795  modfsummod  15961  mertenslem1  16053  sin01gt0  16358  cos01gt0  16359  sin02gt0  16360  dvds2addd  16462  dvds2subd  16463  dvdstrd  16465  bezoutlem4  16715  mulgcd  16721  lcmgcdeq  16787  mulgcddvds  16830  rpmulgcd2  16831  rpdvds  16835  divgcdcoprmex  16841  phimullem  16956  eulerthlem1  16958  eulerthlem2  16959  prmdiveq  16963  pythagtriplem4  16997  pcqmul  17031  pcgcd1  17055  pcadd  17067  pockthlem  17083  prmreclem2  17095  4sqlem16  17138  ramub1lem1  17204  ramub1lem2  17205  prmgaplem7  17235  iscatd2  17855  cicsym  17979  initoeu2  18191  joinval  18549  meetval  18563  lattrd  18620  latledi  18651  mulgass  19321  gaorber  19522  psgnunilem4  19711  efgredlem  19961  odadd2  20063  dmdprdpr  20265  ablfacrp2  20283  ablfac1b  20286  ablfac1eu  20289  pgpfac1  20296  orngmul  21122  ssdifidlprm  21642  gsumbagdiaglem  22239  mdetunilem1  22927  mdetunilem4  22930  mdetunilem9  22935  neiptoptop  23449  lmcnp  23622  txcls  23923  txlly  23955  txnlly  23956  tx1stc  23969  alexsubALTlem1  24366  prdsmet  24689  blin2  24748  blcvx  25117  tgqioo  25119  metnrmlem3  25181  iscmet3lem2  25613  ovolmge0  25798  ovolunlem2  25819  mbfi1flimlem  26043  mbfmullem  26046  itg2add  26080  dvferm1lem  26304  dvferm2lem  26306  dvlip2  26315  dvge0  26326  dvcvx  26340  dvfsumabs  26343  ftc1a  26357  plyadd  26536  plymul  26537  dgrlb  26555  plydivlem4  26617  vieta1lem2  26634  ulmdvlem3  26729  sinq12gt0  26836  logdivlti  26948  fsumharmonic  27339  mpodvdsmulf1o  27521  dvdsmulf1o  27523  logfacubnd  27548  perfectlem1  27556  dchrptlem2  27592  2sqlem5  27749  2sqlem8  27753  2sqmod  27763  dchrisum0flblem2  27836  pntibndlem2  27918  pntlemr  27929  pntlemp  27937  flt4lem2  27977  flt4lem5f  27987  nosupbnd1  28071  nosupbnd2lem1  28072  nosupbnd2  28073  noinfbnd1  28086  noinfbnd2lem1  28087  noinfbnd2  28088  noetasuplem4  28093  noetainflem4  28097  ltstrd  28120  ltlestrd  28121  leltstrd  28122  lestrd  28123  oldbdayim  28275  mulsproplem5  28506  mulsproplem6  28507  mulsproplem7  28508  mulsproplem8  28509  ltmulsd  28523  bdayfinbndlem1  28853  bdayfinbnd  28855  axtgpasch  28929  tgjustr  28936  wlkcompim  30212  wwlksnredwwlkn  30484  wwlksnextsurj  30489  upgr4cycl4dv4e  30786  ex-natded5.2-2  31006  chscllem2  32240  chscllem4  32242  nmopge0  32513  nmfnge0  32529  nmoptrii  32696  staddi  32848  stadd3i  32850  atcvatlem  32987  xrofsup  33401  xrge0addgt0  33620  archiabllem2c  33798  linds2eq  33978  lbsdiflsp0  34300  fedgmullem2  34304  esumpmono  34753  unelldsys  34833  omssubaddlem  34973  signstfvneq0  35243  axtgupdim2ALTV  35339  bnj1098  35456  bnj1110  35654  bnj1121  35657  cplgredgex  35947  erdszelem8  36005  txsconn  36048  cvmlift2lem10  36119  cvmlift3lem7  36132  dfon2lem6  36592  dfon2lem8  36594  cgrtr4d  36792  cgrtrand  36800  cgrtr3and  36802  cgrextendand  36816  btwnexch3and  36828  btwnexchand  36833  linecgrand  36889  endofsegidand  36893  btwnconn1lem4  36897  btwnconn1lem8  36901  btwnconn1lem11  36904  btwnconn1lem12  36905  brsegle2  36916  seglecgr12im  36917  segleantisym  36922  colinbtwnle  36925  broutsideof2  36929  outsideoftr  36936  outsidele  36939  lineelsb2  36955  linethru  36960  ontr2d  36991  ltnadd  37009  gtinf  37149  weiunpo  37295  copsex2d  38103  relowlssretop  38329  pibt2  38383  heicant  38616  mbfresfi  38627  ftc1anclem6  38659  eqvreltrd  39667  riotasv2d  40057  lcvnbtwn2  40127  lcvnbtwn3  40128  lcvexchlem4  40137  omlfh1N  40358  atlen0  40410  atlatmstc  40419  cvratlem  40521  lnnat  40527  2atlt  40539  athgt  40556  1cvratex  40573  ps-2  40578  llncmp  40622  llncvrlpln  40658  lplncmp  40662  lplncvrlvol  40716  lvolcmp  40717  dalemcea  40760  dalem-cly  40771  dalem10  40773  dalem17  40780  dalem25  40798  dalem38  40810  dalem44  40816  dalem55  40827  2atm2atN  40885  cdlema1N  40891  paddasslem5  40924  dalawlem3  40973  dalawlem7  40977  dalawlem11  40981  dalawlem12  40982  lhp0lt  41103  4atexlemc  41169  cdlemg33a  41806  cdlemg33  41811  cdlemk51  42053  dia2dimlem2  42165  dia2dimlem3  42166  dihmeetlem20N  42426  coprmdvds2d  43094  ismrcd2  43753  pellqrex  43929  jm2.17b  44011  jm2.26lem3  44051  omabs2  44377  addrcom  45500  infxrunb2  46422  0ellimcdiv  46702  dvnprodlem1  46999  stoweidlem15  47068  stoweidlem26  47079  stoweidlem28  47081  stoweidlem32  47085  stoweidlem44  47097  meadjuni  47510  dfatcolem  48368  icceuelpart  48561  perfectALTVlem1  48862  bgoldbtbndlem2  48947  bgoldbtbndlem3  48948  copisnmnd  49309  assintopass  49354  lcoss  49591  islindeps2  49638  isldepslvec2  49640  isisod  50178  euendfunc  50677