Theorem mpand 703

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

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

Assertion

Ref	Expression
mpand	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem mpand

Step	Hyp	Ref	Expression
1		mpand.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpand.2	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	ancomsd 468	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 702	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpani  704  mp2and  707  disjss3  5089  sotri2  6102  fpropnf1  7236  ovig  7527  orduniorsuc  7795  resf1ext2b  7901  omopth2  8537  onomeneq  9167  frfi  9214  ordunifi  9219  finsschain  9288  cantnfp1lem3  9621  cantnfp1  9622  p1le  12022  nnge1  12227  zltp1le  12607  gtndiv  12636  uzss  12848  uzm1  12859  addlelt  13095  xrre2  13159  xrre3  13160  xrmaxlt  13170  xrmaxle  13172  xrsupsslem  13296  xrub  13301  supxrunb1  13308  zltaddlt1le  13495  nn0p1elfzo  13694  flflp1  13803  ceile  13845  modfzo0difsn  13942  seqf1olem1  14040  leexp2r  14173  expnlbnd2  14233  facavg  14300  wrdred1hash  14560  ccat2s1fvw  14638  caubnd2  15357  limsupbnd1  15481  limsupbnd2  15482  rlim2lt  15496  rlim3  15497  o1co  15585  mulcn2  15595  cn1lem  15597  rlimo1  15616  climsqz  15640  climsqz2  15641  rlimsqzlem  15648  lo1le  15651  rlimno1  15653  climsup  15669  caucvgrlem2  15674  iseraltlem2  15682  iseralt  15684  fsumabs  15801  cvgcmp  15816  cvgcmpce  15818  isumltss  15850  cvgrat  15885  ruclem9  16242  ruclem12  16245  bitsfzolem  16440  bitsfzo  16441  sadcaddlem  16463  gcdzeq  16558  algcvgblem  16583  algcvga  16585  lcmdvdsb  16619  lcmftp  16642  coprm  16718  eulerthlem2  16789  pclem  16846  infpn2  16921  prmreclem1  16924  prmreclem4  16927  ramtlecl  17008  prmgaplem7  17065  initoeu2  18021  lubval  18358  lublecllem  18362  glbval  18371  joinle  18388  latmlem1  18473  odmulg  19568  efginvrel2  19739  pgpfac1lem5  20093  chfacfscmul0  22887  chfacfpmmul0  22891  1stccnp  23491  qustgplem  24150  imasdsf1olem  24402  bldisj  24427  xbln0  24443  prdsbl  24520  metss2lem  24540  stdbdxmet  24544  ngptgp  24665  nghmcn  24774  icoopnst  24970  iocopnst  24971  cnllycmp  24987  iscau3  25309  cmetcaulem  25319  iscmet3lem1  25322  bcthlem4  25358  ovollb2lem  25519  ovolicc2lem3  25550  voliunlem3  25583  volcn  25637  itg10a  25741  itg1ge0a  25742  bddiblnc  25873  dvcnvrelem1  26048  dvfsumrlim  26062  itgsubst  26080  ulmcn  26428  ulmdvlem3  26431  mtest  26433  tanord  26569  emcllem6  27031  ftalem2  27104  chtub  27242  fsumvma2  27244  vmasum  27246  chpchtsum  27249  bcmono  27307  bclbnd  27310  bposlem1  27314  bposlem5  27318  bposlem6  27319  lgsne0  27365  gausslemma2dlem1a  27395  chtppilim  27505  dchrisumlem3  27521  pntrsumbnd2  27597  pntlemf  27635  pntlem3  27639  pntleml  27641  nosupno  27733  noinfno  27748  mulsproplem6  28180  mulsproplem7  28181  upgr2pthnlp  29867  crctcshwlkn0lem3  29947  crctcshwlkn0lem5  29949  eupth2lems  30375  grpoidinvlem3  30644  grpoideu  30647  vacn  30832  blocni  30943  ubthlem2  31009  chscllem2  31776  lnconi  32171  pjnmopi  32286  atomli  32520  sumdmdlem2  32557  cdj3lem2b  32575  xraddge02  32898  fedgmullem1  33870  dfon2lem5  36073  dfon2lem6  36074  cgrcoml  36284  btwnconn2  36390  fvineqsneq  37844  pibt2  37849  ltflcei  38045  poimirlem2  38059  poimirlem18  38075  poimirlem22  38079  poimirlem23  38080  poimirlem26  38083  poimirlem29  38086  poimirlem30  38087  poimirlem32  38089  heicant  38092  mblfinlem3  38096  mblfinlem4  38097  itg2addnclem  38108  itg2addnc  38111  ftc1anclem6  38135  ftc1anc  38138  mettrifi  38194  geomcau  38196  equivbnd  38227  heibor1lem  38246  bfplem1  38259  bfplem2  38260  rrncmslem  38269  divrngidl  38465  preuniqval  38933  lecmtN  39818  cvrletrN  39835  llnnleat  40075  lplnnle2at  40103  lvolnle3at  40144  dalem21  40256  cdlemblem  40355  osumcllem11N  40528  pexmidlem8N  40539  lhpmcvr4N  40588  cdleme32b  41004  cdleme35fnpq  41011  cdleme48bw  41064  cdlemf1  41123  cdlemg2fv2  41162  cdlemg7fvbwN  41169  cdlemg27b  41258  tendoeq2  41336  dia2dimlem1  41626  dihord6apre  41818  dihord5apre  41824  dihglbcpreN  41862  dochnel2  41954  dihjat1lem  41990  dochexmidlem8  42029  mapdordlem2  42199  eqresfnbd  42789  3cubeslem1  43203  ordnexbtwnsuc  43782  naddcnfid2  43883  nadd2rabex  43901  iscard5  44050  frege124d  44275  mnringmulrcld  44742  climinf  46120  2ffzoeq  47860  iccpartlt  47968  lighneallem2  48153  bgoldbtbndlem3  48367  bgoldbtbndlem4  48368  tgoldbach  48377  fllog2  49128  dignn0ldlem  49162