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  5146  sotri2  6151  fpropnf1  7286  ovig  7578  orduniorsuc  7849  omopth2  8620  onomeneq  9262  frfi  9318  ordunifi  9323  finsschain  9396  cantnfp1lem3  9717  cantnfp1  9718  p1le  12109  nnge1  12291  zltp1le  12664  gtndiv  12692  uzss  12898  eluzaddOLD  12910  uzm1  12913  addlelt  13146  xrre2  13208  xrre3  13209  xrmaxlt  13219  xrmaxle  13221  xrsupsslem  13345  xrub  13350  supxrunb1  13357  zltaddlt1le  13541  nn0p1elfzo  13738  flflp1  13843  ceile  13885  modfzo0difsn  13980  seqf1olem1  14078  leexp2r  14210  expnlbnd2  14269  facavg  14336  wrdred1hash  14595  ccat2s1fvw  14672  caubnd2  15392  limsupbnd1  15514  limsupbnd2  15515  rlim2lt  15529  rlim3  15530  o1co  15618  mulcn2  15628  cn1lem  15630  rlimo1  15649  climsqz  15673  climsqz2  15674  rlimsqzlem  15681  lo1le  15684  rlimno1  15686  climsup  15702  caucvgrlem2  15707  iseraltlem2  15715  iseralt  15717  fsumabs  15833  cvgcmp  15848  cvgcmpce  15850  isumltss  15880  cvgrat  15915  ruclem9  16270  ruclem12  16273  bitsfzolem  16467  bitsfzo  16468  sadcaddlem  16490  gcdzeq  16585  algcvgblem  16610  algcvga  16612  lcmdvdsb  16646  lcmftp  16669  coprm  16744  eulerthlem2  16815  pclem  16871  infpn2  16946  prmreclem1  16949  prmreclem4  16952  ramtlecl  17033  prmgaplem7  17090  initoeu2  18069  lubval  18413  lublecllem  18417  glbval  18426  joinle  18443  latmlem1  18526  odmulg  19588  efginvrel2  19759  pgpfac1lem5  20113  chfacfscmul0  22879  chfacfpmmul0  22883  1stccnp  23485  qustgplem  24144  imasdsf1olem  24398  bldisj  24423  xbln0  24439  prdsbl  24519  metss2lem  24539  stdbdxmet  24543  ngptgp  24664  nghmcn  24781  icoopnst  24982  iocopnst  24983  cnllycmp  25001  iscau3  25325  cmetcaulem  25335  iscmet3lem1  25338  bcthlem4  25374  ovollb2lem  25536  ovolicc2lem3  25567  voliunlem3  25600  volcn  25654  itg10a  25759  itg1ge0a  25760  bddiblnc  25891  dvcnvrelem1  26070  dvfsumrlim  26086  itgsubst  26104  ulmcn  26456  ulmdvlem3  26459  mtest  26461  tanord  26594  emcllem6  27058  ftalem2  27131  chtub  27270  fsumvma2  27272  vmasum  27274  chpchtsum  27277  bcmono  27335  bclbnd  27338  bposlem1  27342  bposlem5  27346  bposlem6  27347  lgsne0  27393  gausslemma2dlem1a  27423  chtppilim  27533  dchrisumlem3  27549  pntrsumbnd2  27625  pntlemf  27663  pntlem3  27667  pntleml  27669  nosupno  27762  noinfno  27777  mulsproplem6  28161  mulsproplem7  28162  upgr2pthnlp  29764  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  eupth2lems  30266  grpoidinvlem3  30534  grpoideu  30537  vacn  30722  blocni  30833  ubthlem2  30899  chscllem2  31666  lnconi  32061  pjnmopi  32176  atomli  32410  sumdmdlem2  32447  cdj3lem2b  32465  xraddge02  32766  fedgmullem1  33656  dfon2lem5  35768  dfon2lem6  35769  cgrcoml  35977  btwnconn2  36083  fvineqsneq  37394  pibt2  37399  ltflcei  37594  poimirlem2  37608  poimirlem18  37624  poimirlem22  37628  poimirlem23  37629  poimirlem26  37632  poimirlem29  37635  poimirlem30  37636  poimirlem32  37638  heicant  37641  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem  37657  itg2addnc  37660  ftc1anclem6  37684  ftc1anc  37687  mettrifi  37743  geomcau  37745  equivbnd  37776  heibor1lem  37795  bfplem1  37808  bfplem2  37809  rrncmslem  37818  divrngidl  38014  lecmtN  39237  cvrletrN  39254  llnnleat  39495  lplnnle2at  39523  lvolnle3at  39564  dalem21  39676  cdlemblem  39775  osumcllem11N  39948  pexmidlem8N  39959  lhpmcvr4N  40008  cdleme32b  40424  cdleme35fnpq  40431  cdleme48bw  40484  cdlemf1  40543  cdlemg2fv2  40582  cdlemg7fvbwN  40589  cdlemg27b  40678  tendoeq2  40756  dia2dimlem1  41046  dihord6apre  41238  dihord5apre  41244  dihglbcpreN  41282  dochnel2  41374  dihjat1lem  41410  dochexmidlem8  41449  mapdordlem2  41619  eqresfnbd  42251  3cubeslem1  42671  ordnexbtwnsuc  43256  naddcnfid2  43357  nadd2rabex  43375  iscard5  43525  frege124d  43750  mnringmulrcld  44223  climinf  45561  2ffzoeq  47276  iccpartlt  47348  lighneallem2  47530  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  tgoldbach  47741  fllog2  48417  dignn0ldlem  48451