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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  mpani  696  mp2and  699  ecase2dOLD  1031  disjss3  5038  sotri2  5974  fpropnf1  7057  ovig  7333  orduniorsuc  7587  omopth2  8290  frfi  8894  ordunifi  8899  finsschain  8961  cantnfp1lem3  9273  cantnfp1  9274  p1le  11642  nnge1  11823  zltp1le  12192  gtndiv  12219  uzss  12426  eluzadd  12434  uzm1  12437  addlelt  12665  xrre2  12725  xrre3  12726  xrmaxlt  12736  xrmaxle  12738  xrsupsslem  12862  xrub  12867  supxrunb1  12874  zltaddlt1le  13058  nn0p1elfzo  13250  elfzoext  13264  flflp1  13347  ceile  13387  modfzo0difsn  13481  seqf1olem1  13580  leexp2r  13709  expnlbnd2  13766  facavg  13832  wrdred1hash  14081  ccat2s1fvw  14166  ccat2s1fvwOLD  14167  caubnd2  14886  limsupbnd1  15008  limsupbnd2  15009  rlim2lt  15023  rlim3  15024  o1co  15112  mulcn2  15122  cn1lem  15124  rlimo1  15143  climsqz  15167  climsqz2  15168  rlimsqzlem  15177  lo1le  15180  rlimno1  15182  climsup  15198  caucvgrlem2  15203  iseraltlem2  15211  iseralt  15213  fsumabs  15328  cvgcmp  15343  cvgcmpce  15345  isumltss  15375  cvgrat  15410  ruclem9  15762  ruclem12  15765  bitsfzolem  15956  bitsfzo  15957  sadcaddlem  15979  gcdzeq  16077  algcvgblem  16097  algcvga  16099  lcmdvdsb  16133  lcmftp  16156  coprm  16231  eulerthlem2  16298  pclem  16354  infpn2  16429  prmreclem1  16432  prmreclem4  16435  ramtlecl  16516  prmgaplem7  16573  initoeu2  17476  lubval  17816  lublecllem  17820  glbval  17829  joinle  17846  latmlem1  17929  odmulg  18901  efginvrel2  19071  pgpfac1lem5  19420  chfacfscmul0  21709  chfacfpmmul0  21713  1stccnp  22313  qustgplem  22972  imasdsf1olem  23225  bldisj  23250  xbln0  23266  prdsbl  23343  metss2lem  23363  stdbdxmet  23367  ngptgp  23488  nghmcn  23597  icoopnst  23790  iocopnst  23791  cnllycmp  23807  iscau3  24129  cmetcaulem  24139  iscmet3lem1  24142  bcthlem4  24178  ovollb2lem  24339  ovolicc2lem3  24370  voliunlem3  24403  volcn  24457  itg10a  24562  itg1ge0a  24563  bddiblnc  24693  dvcnvrelem1  24868  dvfsumrlim  24882  itgsubst  24900  ulmcn  25245  ulmdvlem3  25248  mtest  25250  tanord  25381  emcllem6  25837  ftalem2  25910  chtub  26047  fsumvma2  26049  vmasum  26051  chpchtsum  26054  bcmono  26112  bclbnd  26115  bposlem1  26119  bposlem5  26123  bposlem6  26124  lgsne0  26170  gausslemma2dlem1a  26200  chtppilim  26310  dchrisumlem3  26326  pntrsumbnd2  26402  pntlemf  26440  pntlem3  26444  pntleml  26446  upgr2pthnlp  27773  crctcshwlkn0lem3  27850  crctcshwlkn0lem5  27852  eupth2lems  28275  grpoidinvlem3  28541  grpoideu  28544  vacn  28729  blocni  28840  ubthlem2  28906  chscllem2  29673  lnconi  30068  pjnmopi  30183  atomli  30417  sumdmdlem2  30454  cdj3lem2b  30472  xraddge02  30753  fedgmullem1  31378  dfon2lem5  33433  dfon2lem6  33434  nosupno  33592  noinfno  33607  cgrcoml  33984  btwnconn2  34090  fvineqsneq  35269  pibt2  35274  ltflcei  35451  poimirlem2  35465  poimirlem18  35481  poimirlem22  35485  poimirlem23  35486  poimirlem26  35489  poimirlem29  35492  poimirlem30  35493  poimirlem32  35495  heicant  35498  mblfinlem3  35502  mblfinlem4  35503  itg2addnclem  35514  itg2addnc  35517  ftc1anclem6  35541  ftc1anc  35544  mettrifi  35601  geomcau  35603  equivbnd  35634  heibor1lem  35653  bfplem1  35666  bfplem2  35667  rrncmslem  35676  divrngidl  35872  lecmtN  36956  cvrletrN  36973  llnnleat  37213  lplnnle2at  37241  lvolnle3at  37282  dalem21  37394  cdlemblem  37493  osumcllem11N  37666  pexmidlem8N  37677  lhpmcvr4N  37726  cdleme32b  38142  cdleme35fnpq  38149  cdleme48bw  38202  cdlemf1  38261  cdlemg2fv2  38300  cdlemg7fvbwN  38307  cdlemg27b  38396  tendoeq2  38474  dia2dimlem1  38764  dihord6apre  38956  dihord5apre  38962  dihglbcpreN  39000  dochnel2  39092  dihjat1lem  39128  dochexmidlem8  39167  mapdordlem2  39337  3cubeslem1  40150  iscard5  40767  frege124d  40987  mnringmulrcld  41460  climinf  42765  2ffzoeq  44436  iccpartlt  44492  lighneallem2  44674  bgoldbtbndlem3  44875  bgoldbtbndlem4  44876  tgoldbach  44885  fllog2  45530  dignn0ldlem  45564