Theorem mpand 708

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 471	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 707	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:  mpani  709  mp2and  712  disjss3  5105  sotri2  6135  fpropnf1  7294  ovig  7590  orduniorsuc  7865  resf1ext2b  7971  omopth2  8620  onomeneq  9257  frfi  9304  ordunifi  9309  finsschain  9376  cantnfp1lem3  9708  cantnfp1  9709  p1le  12189  nnge1  12393  zltp1le  12773  gtndiv  12803  uzss  13015  uzm1  13026  addlelt  13263  xrre2  13327  xrre3  13328  xrmaxlt  13338  xrmaxle  13340  xrsupsslem  13464  xrub  13469  supxrunb1  13476  zltaddlt1le  13663  nn0p1elfzo  13864  flflp1  13974  ceile  14016  modfzo0difsn  14113  seqf1olem1  14211  leexp2r  14344  expnlbnd2  14405  facavg  14472  wrdred1hash  14733  ccat2s1fvw  14814  caubnd2  15554  limsupbnd1  15678  limsupbnd2  15679  rlim2lt  15693  rlim3  15694  o1co  15782  mulcn2  15792  cn1lem  15794  rlimo1  15813  climsqz  15837  climsqz2  15838  rlimsqzlem  15845  lo1le  15848  rlimno1  15850  climsup  15866  caucvgrlem2  15871  iseraltlem2  15879  iseralt  15881  fsumabs  15997  cvgcmp  16012  cvgcmpce  16014  isumltss  16046  cvgrat  16081  ruclem9  16435  ruclem12  16438  bitsfzolem  16633  bitsfzo  16634  sadcaddlem  16656  gcdzeq  16754  algcvgblem  16781  algcvga  16783  lcmdvdsb  16817  lcmftp  16840  coprm  16916  eulerthlem2  16988  pclem  17045  infpn2  17120  prmreclem1  17123  prmreclem4  17126  ramtlecl  17207  prmgaplem7  17264  initoeu2  18220  lubval  18557  lublecllem  18561  glbval  18570  joinle  18587  latmlem1  18672  odmulg  19800  efginvrel2  19971  pgpfac1lem5  20325  chfacfscmul0  23206  chfacfpmmul0  23210  1stccnp  23811  qustgplem  24470  imasdsf1olem  24722  bldisj  24747  xbln0  24763  prdsbl  24840  metss2lem  24860  stdbdxmet  24864  ngptgp  24985  nghmcn  25094  icoopnst  25290  iocopnst  25291  cnllycmp  25307  iscau3  25629  cmetcaulem  25639  iscmet3lem1  25642  bcthlem4  25678  ovollb2lem  25839  ovolicc2lem3  25870  voliunlem3  25903  volcn  25957  itg10a  26061  itg1ge0a  26062  bddiblnc  26192  dvcnvrelem1  26367  dvfsumrlim  26381  itgsubst  26399  ulmcn  26756  ulmdvlem3  26759  mtest  26761  tanord  26896  emcllem6  27358  ftalem2  27431  chtub  27569  fsumvma2  27571  vmasum  27573  chpchtsum  27576  bcmono  27634  bclbnd  27637  bposlem1  27641  bposlem5  27645  bposlem6  27646  lgsne0  27692  gausslemma2dlem1a  27722  chtppilim  27832  dchrisumlem3  27848  pntrsumbnd2  27924  pntlemf  27962  pntlem3  27966  pntleml  27968  nosupno  28090  noinfno  28105  mulsproplem6  28537  mulsproplem7  28538  upgr2pthnlp  30348  crctcshwlkn0lem3  30431  crctcshwlkn0lem5  30433  eupth2lems  30869  grpoidinvlem3  31138  grpoideu  31141  vacn  31326  blocni  31437  ubthlem2  31503  chscllem2  32270  lnconi  32665  pjnmopi  32780  atomli  33014  sumdmdlem2  33051  cdj3lem2b  33069  xraddge02  33419  fedgmullem1  34331  maxssj0  36006  dfon2lem5  36727  dfon2lem6  36728  cgrcoml  36939  btwnconn2  37045  fvineqsneq  38527  pibt2  38532  ltflcei  38723  poimirlem2  38732  poimirlem18  38748  poimirlem22  38752  poimirlem23  38753  poimirlem26  38756  poimirlem29  38759  poimirlem30  38760  poimirlem32  38762  heicant  38765  mblfinlem3  38769  mblfinlem4  38770  itg2addnclem  38781  itg2addnc  38784  ftc1anclem6  38808  ftc1anc  38811  mettrifi  38883  geomcau  38885  equivbnd  38916  heibor1lem  38935  bfplem1  38948  bfplem2  38949  rrncmslem  38958  divrngidl  39154  preuniqval  39620  lecmtN  40505  cvrletrN  40522  llnnleat  40762  lplnnle2at  40790  lvolnle3at  40831  dalem21  40943  cdlemblem  41042  osumcllem11N  41215  pexmidlem8N  41226  lhpmcvr4N  41275  cdleme32b  41691  cdleme35fnpq  41698  cdleme48bw  41751  cdlemf1  41810  cdlemg2fv2  41849  cdlemg7fvbwN  41856  cdlemg27b  41945  tendoeq2  42023  dia2dimlem1  42313  dihord6apre  42505  dihord5apre  42511  dihglbcpreN  42549  dochnel2  42641  dihjat1lem  42677  dochexmidlem8  42716  mapdordlem2  42886  eqresfnbd  43479  3cubeslem1  43887  ordnexbtwnsuc  44461  naddcnfid2  44562  nadd2rabex  44580  iscard5  44729  frege124d  44953  mnringmulrcld  45418  climinf  46823  2ffzoeq  48603  iccpartlt  48711  lighneallem2  48896  bgoldbtbndlem3  49110  bgoldbtbndlem4  49111  tgoldbach  49120  fllog2  49885  dignn0ldlem  49919