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  5142  sotri2  6149  fpropnf1  7287  ovig  7579  orduniorsuc  7850  resf1ext2b  7957  omopth2  8622  onomeneq  9265  frfi  9321  ordunifi  9326  finsschain  9399  cantnfp1lem3  9720  cantnfp1  9721  p1le  12112  nnge1  12294  zltp1le  12667  gtndiv  12695  uzss  12901  eluzaddOLD  12913  uzm1  12916  addlelt  13149  xrre2  13212  xrre3  13213  xrmaxlt  13223  xrmaxle  13225  xrsupsslem  13349  xrub  13354  supxrunb1  13361  zltaddlt1le  13545  nn0p1elfzo  13742  flflp1  13847  ceile  13889  modfzo0difsn  13984  seqf1olem1  14082  leexp2r  14214  expnlbnd2  14273  facavg  14340  wrdred1hash  14599  ccat2s1fvw  14676  caubnd2  15396  limsupbnd1  15518  limsupbnd2  15519  rlim2lt  15533  rlim3  15534  o1co  15622  mulcn2  15632  cn1lem  15634  rlimo1  15653  climsqz  15677  climsqz2  15678  rlimsqzlem  15685  lo1le  15688  rlimno1  15690  climsup  15706  caucvgrlem2  15711  iseraltlem2  15719  iseralt  15721  fsumabs  15837  cvgcmp  15852  cvgcmpce  15854  isumltss  15884  cvgrat  15919  ruclem9  16274  ruclem12  16277  bitsfzolem  16471  bitsfzo  16472  sadcaddlem  16494  gcdzeq  16589  algcvgblem  16614  algcvga  16616  lcmdvdsb  16650  lcmftp  16673  coprm  16748  eulerthlem2  16819  pclem  16876  infpn2  16951  prmreclem1  16954  prmreclem4  16957  ramtlecl  17038  prmgaplem7  17095  initoeu2  18061  lubval  18401  lublecllem  18405  glbval  18414  joinle  18431  latmlem1  18514  odmulg  19574  efginvrel2  19745  pgpfac1lem5  20099  chfacfscmul0  22864  chfacfpmmul0  22868  1stccnp  23470  qustgplem  24129  imasdsf1olem  24383  bldisj  24408  xbln0  24424  prdsbl  24504  metss2lem  24524  stdbdxmet  24528  ngptgp  24649  nghmcn  24766  icoopnst  24969  iocopnst  24970  cnllycmp  24988  iscau3  25312  cmetcaulem  25322  iscmet3lem1  25325  bcthlem4  25361  ovollb2lem  25523  ovolicc2lem3  25554  voliunlem3  25587  volcn  25641  itg10a  25745  itg1ge0a  25746  bddiblnc  25877  dvcnvrelem1  26056  dvfsumrlim  26072  itgsubst  26090  ulmcn  26442  ulmdvlem3  26445  mtest  26447  tanord  26580  emcllem6  27044  ftalem2  27117  chtub  27256  fsumvma2  27258  vmasum  27260  chpchtsum  27263  bcmono  27321  bclbnd  27324  bposlem1  27328  bposlem5  27332  bposlem6  27333  lgsne0  27379  gausslemma2dlem1a  27409  chtppilim  27519  dchrisumlem3  27535  pntrsumbnd2  27611  pntlemf  27649  pntlem3  27653  pntleml  27655  nosupno  27748  noinfno  27763  mulsproplem6  28147  mulsproplem7  28148  upgr2pthnlp  29752  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  eupth2lems  30257  grpoidinvlem3  30525  grpoideu  30528  vacn  30713  blocni  30824  ubthlem2  30890  chscllem2  31657  lnconi  32052  pjnmopi  32167  atomli  32401  sumdmdlem2  32438  cdj3lem2b  32456  xraddge02  32760  fedgmullem1  33680  dfon2lem5  35788  dfon2lem6  35789  cgrcoml  35997  btwnconn2  36103  fvineqsneq  37413  pibt2  37418  ltflcei  37615  poimirlem2  37629  poimirlem18  37645  poimirlem22  37649  poimirlem23  37650  poimirlem26  37653  poimirlem29  37656  poimirlem30  37657  poimirlem32  37659  heicant  37662  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem  37678  itg2addnc  37681  ftc1anclem6  37705  ftc1anc  37708  mettrifi  37764  geomcau  37766  equivbnd  37797  heibor1lem  37816  bfplem1  37829  bfplem2  37830  rrncmslem  37839  divrngidl  38035  lecmtN  39257  cvrletrN  39274  llnnleat  39515  lplnnle2at  39543  lvolnle3at  39584  dalem21  39696  cdlemblem  39795  osumcllem11N  39968  pexmidlem8N  39979  lhpmcvr4N  40028  cdleme32b  40444  cdleme35fnpq  40451  cdleme48bw  40504  cdlemf1  40563  cdlemg2fv2  40602  cdlemg7fvbwN  40609  cdlemg27b  40698  tendoeq2  40776  dia2dimlem1  41066  dihord6apre  41258  dihord5apre  41264  dihglbcpreN  41302  dochnel2  41394  dihjat1lem  41430  dochexmidlem8  41469  mapdordlem2  41639  eqresfnbd  42273  3cubeslem1  42695  ordnexbtwnsuc  43280  naddcnfid2  43381  nadd2rabex  43399  iscard5  43549  frege124d  43774  mnringmulrcld  44247  climinf  45621  2ffzoeq  47339  iccpartlt  47411  lighneallem2  47593  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  tgoldbach  47804  fllog2  48489  dignn0ldlem  48523