Theorem mpand 696

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 695	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  697  mp2and  700  disjss3  5073  sotri2  6081  fpropnf1  7211  ovig  7502  orduniorsuc  7770  resf1ext2b  7875  omopth2  8508  onomeneq  9137  frfi  9184  ordunifi  9189  finsschain  9258  cantnfp1lem3  9590  cantnfp1  9591  p1le  11989  nnge1  12194  zltp1le  12566  gtndiv  12595  uzss  12800  uzm1  12811  addlelt  13047  xrre2  13111  xrre3  13112  xrmaxlt  13122  xrmaxle  13124  xrsupsslem  13248  xrub  13253  supxrunb1  13260  zltaddlt1le  13447  nn0p1elfzo  13646  flflp1  13755  ceile  13797  modfzo0difsn  13894  seqf1olem1  13992  leexp2r  14125  expnlbnd2  14185  facavg  14252  wrdred1hash  14512  ccat2s1fvw  14590  caubnd2  15309  limsupbnd1  15433  limsupbnd2  15434  rlim2lt  15448  rlim3  15449  o1co  15537  mulcn2  15547  cn1lem  15549  rlimo1  15568  climsqz  15592  climsqz2  15593  rlimsqzlem  15600  lo1le  15603  rlimno1  15605  climsup  15621  caucvgrlem2  15626  iseraltlem2  15634  iseralt  15636  fsumabs  15753  cvgcmp  15768  cvgcmpce  15770  isumltss  15802  cvgrat  15837  ruclem9  16194  ruclem12  16197  bitsfzolem  16392  bitsfzo  16393  sadcaddlem  16415  gcdzeq  16510  algcvgblem  16535  algcvga  16537  lcmdvdsb  16571  lcmftp  16594  coprm  16670  eulerthlem2  16741  pclem  16798  infpn2  16873  prmreclem1  16876  prmreclem4  16879  ramtlecl  16960  prmgaplem7  17017  initoeu2  17972  lubval  18309  lublecllem  18313  glbval  18322  joinle  18339  latmlem1  18424  odmulg  19520  efginvrel2  19691  pgpfac1lem5  20045  chfacfscmul0  22811  chfacfpmmul0  22815  1stccnp  23415  qustgplem  24074  imasdsf1olem  24326  bldisj  24351  xbln0  24367  prdsbl  24444  metss2lem  24464  stdbdxmet  24468  ngptgp  24589  nghmcn  24698  icoopnst  24894  iocopnst  24895  cnllycmp  24911  iscau3  25233  cmetcaulem  25243  iscmet3lem1  25246  bcthlem4  25282  ovollb2lem  25443  ovolicc2lem3  25474  voliunlem3  25507  volcn  25561  itg10a  25665  itg1ge0a  25666  bddiblnc  25797  dvcnvrelem1  25972  dvfsumrlim  25986  itgsubst  26004  ulmcn  26352  ulmdvlem3  26355  mtest  26357  tanord  26490  emcllem6  26952  ftalem2  27025  chtub  27163  fsumvma2  27165  vmasum  27167  chpchtsum  27170  bcmono  27228  bclbnd  27231  bposlem1  27235  bposlem5  27239  bposlem6  27240  lgsne0  27286  gausslemma2dlem1a  27316  chtppilim  27426  dchrisumlem3  27442  pntrsumbnd2  27518  pntlemf  27556  pntlem3  27560  pntleml  27562  nosupno  27655  noinfno  27670  mulsproplem6  28101  mulsproplem7  28102  upgr2pthnlp  29788  crctcshwlkn0lem3  29868  crctcshwlkn0lem5  29870  eupth2lems  30296  grpoidinvlem3  30565  grpoideu  30568  vacn  30753  blocni  30864  ubthlem2  30930  chscllem2  31697  lnconi  32092  pjnmopi  32207  atomli  32441  sumdmdlem2  32478  cdj3lem2b  32496  xraddge02  32818  fedgmullem1  33761  dfon2lem5  35955  dfon2lem6  35956  cgrcoml  36166  btwnconn2  36272  fvineqsneq  37716  pibt2  37721  ltflcei  37917  poimirlem2  37931  poimirlem18  37947  poimirlem22  37951  poimirlem23  37952  poimirlem26  37955  poimirlem29  37958  poimirlem30  37959  poimirlem32  37961  heicant  37964  mblfinlem3  37968  mblfinlem4  37969  itg2addnclem  37980  itg2addnc  37983  ftc1anclem6  38007  ftc1anc  38010  mettrifi  38066  geomcau  38068  equivbnd  38099  heibor1lem  38118  bfplem1  38131  bfplem2  38132  rrncmslem  38141  divrngidl  38337  preuniqval  38805  lecmtN  39690  cvrletrN  39707  llnnleat  39947  lplnnle2at  39975  lvolnle3at  40016  dalem21  40128  cdlemblem  40227  osumcllem11N  40400  pexmidlem8N  40411  lhpmcvr4N  40460  cdleme32b  40876  cdleme35fnpq  40883  cdleme48bw  40936  cdlemf1  40995  cdlemg2fv2  41034  cdlemg7fvbwN  41041  cdlemg27b  41130  tendoeq2  41208  dia2dimlem1  41498  dihord6apre  41690  dihord5apre  41696  dihglbcpreN  41734  dochnel2  41826  dihjat1lem  41862  dochexmidlem8  41901  mapdordlem2  42071  eqresfnbd  42661  3cubeslem1  43104  ordnexbtwnsuc  43683  naddcnfid2  43784  nadd2rabex  43802  iscard5  43951  frege124d  44176  mnringmulrcld  44643  climinf  46024  2ffzoeq  47764  iccpartlt  47872  lighneallem2  48057  bgoldbtbndlem3  48271  bgoldbtbndlem4  48272  tgoldbach  48281  fllog2  49032  dignn0ldlem  49066