Theorem mpand 695

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 465	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 694	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpani  696  mp2and  699  disjss3  5094  sotri2  6082  fpropnf1  7208  ovig  7499  orduniorsuc  7769  resf1ext2b  7875  omopth2  8509  onomeneq  9138  frfi  9190  ordunifi  9195  finsschain  9268  cantnfp1lem3  9595  cantnfp1  9596  p1le  11987  nnge1  12174  zltp1le  12543  gtndiv  12571  uzss  12776  eluzaddOLD  12788  uzm1  12791  addlelt  13027  xrre2  13090  xrre3  13091  xrmaxlt  13101  xrmaxle  13103  xrsupsslem  13227  xrub  13232  supxrunb1  13239  zltaddlt1le  13426  nn0p1elfzo  13623  flflp1  13729  ceile  13771  modfzo0difsn  13868  seqf1olem1  13966  leexp2r  14099  expnlbnd2  14159  facavg  14226  wrdred1hash  14486  ccat2s1fvw  14563  caubnd2  15283  limsupbnd1  15407  limsupbnd2  15408  rlim2lt  15422  rlim3  15423  o1co  15511  mulcn2  15521  cn1lem  15523  rlimo1  15542  climsqz  15566  climsqz2  15567  rlimsqzlem  15574  lo1le  15577  rlimno1  15579  climsup  15595  caucvgrlem2  15600  iseraltlem2  15608  iseralt  15610  fsumabs  15726  cvgcmp  15741  cvgcmpce  15743  isumltss  15773  cvgrat  15808  ruclem9  16165  ruclem12  16168  bitsfzolem  16363  bitsfzo  16364  sadcaddlem  16386  gcdzeq  16481  algcvgblem  16506  algcvga  16508  lcmdvdsb  16542  lcmftp  16565  coprm  16640  eulerthlem2  16711  pclem  16768  infpn2  16843  prmreclem1  16846  prmreclem4  16849  ramtlecl  16930  prmgaplem7  16987  initoeu2  17941  lubval  18278  lublecllem  18282  glbval  18291  joinle  18308  latmlem1  18393  odmulg  19453  efginvrel2  19624  pgpfac1lem5  19978  chfacfscmul0  22761  chfacfpmmul0  22765  1stccnp  23365  qustgplem  24024  imasdsf1olem  24277  bldisj  24302  xbln0  24318  prdsbl  24395  metss2lem  24415  stdbdxmet  24419  ngptgp  24540  nghmcn  24649  icoopnst  24852  iocopnst  24853  cnllycmp  24871  iscau3  25194  cmetcaulem  25204  iscmet3lem1  25207  bcthlem4  25243  ovollb2lem  25405  ovolicc2lem3  25436  voliunlem3  25469  volcn  25523  itg10a  25627  itg1ge0a  25628  bddiblnc  25759  dvcnvrelem1  25938  dvfsumrlim  25954  itgsubst  25972  ulmcn  26324  ulmdvlem3  26327  mtest  26329  tanord  26463  emcllem6  26927  ftalem2  27000  chtub  27139  fsumvma2  27141  vmasum  27143  chpchtsum  27146  bcmono  27204  bclbnd  27207  bposlem1  27211  bposlem5  27215  bposlem6  27216  lgsne0  27262  gausslemma2dlem1a  27292  chtppilim  27402  dchrisumlem3  27418  pntrsumbnd2  27494  pntlemf  27532  pntlem3  27536  pntleml  27538  nosupno  27631  noinfno  27646  mulsproplem6  28047  mulsproplem7  28048  upgr2pthnlp  29695  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  eupth2lems  30200  grpoidinvlem3  30468  grpoideu  30471  vacn  30656  blocni  30767  ubthlem2  30833  chscllem2  31600  lnconi  31995  pjnmopi  32110  atomli  32344  sumdmdlem2  32381  cdj3lem2b  32399  xraddge02  32713  fedgmullem1  33601  dfon2lem5  35760  dfon2lem6  35761  cgrcoml  35969  btwnconn2  36075  fvineqsneq  37385  pibt2  37390  ltflcei  37587  poimirlem2  37601  poimirlem18  37617  poimirlem22  37621  poimirlem23  37622  poimirlem26  37625  poimirlem29  37628  poimirlem30  37629  poimirlem32  37631  heicant  37634  mblfinlem3  37638  mblfinlem4  37639  itg2addnclem  37650  itg2addnc  37653  ftc1anclem6  37677  ftc1anc  37680  mettrifi  37736  geomcau  37738  equivbnd  37769  heibor1lem  37788  bfplem1  37801  bfplem2  37802  rrncmslem  37811  divrngidl  38007  lecmtN  39234  cvrletrN  39251  llnnleat  39492  lplnnle2at  39520  lvolnle3at  39561  dalem21  39673  cdlemblem  39772  osumcllem11N  39945  pexmidlem8N  39956  lhpmcvr4N  40005  cdleme32b  40421  cdleme35fnpq  40428  cdleme48bw  40481  cdlemf1  40540  cdlemg2fv2  40579  cdlemg7fvbwN  40586  cdlemg27b  40675  tendoeq2  40753  dia2dimlem1  41043  dihord6apre  41235  dihord5apre  41241  dihglbcpreN  41279  dochnel2  41371  dihjat1lem  41407  dochexmidlem8  41446  mapdordlem2  41616  eqresfnbd  42205  3cubeslem1  42657  ordnexbtwnsuc  43240  naddcnfid2  43341  nadd2rabex  43359  iscard5  43509  frege124d  43734  mnringmulrcld  44201  climinf  45588  2ffzoeq  47312  iccpartlt  47409  lighneallem2  47591  bgoldbtbndlem3  47792  bgoldbtbndlem4  47793  tgoldbach  47802  fllog2  48541  dignn0ldlem  48575