MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imdistani Structured version   Unicode version

Theorem imdistani 690
Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
imdistani.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
imdistani  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )

Proof of Theorem imdistani
StepHypRef Expression
1 imdistani.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21anc2li 557 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ch ) ) )
32imp 429 1  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  cases2  971  nfan1  1928  2eu1OLD  2377  difrab  3779  rabsnifsb  4100  foconst  5812  elfvmptrab  5978  dffo4  6048  dffo5  6049  isofrlem  6237  onint  6629  tz7.48lem  7124  opthreg  8052  axpowndlem3OLD  8993  eltsk2g  9146  recgt1i  10462  sup2  10519  elnnnn0c  10862  elnnz1  10911  recnz  10959  eluz2b2  11179  iccsplit  11678  elfzp12  11782  1mod  12030  2swrd1eqwrdeq  12690  cos01gt0  13937  reumodprminv  14340  clatl  15872  isacs4lem  15924  isacs5lem  15925  isnzr2hash  18038  mplcoe5lem  18256  ioovolcl  22104  elply2  22718  wlkonprop  24661  trlonprop  24670  pthonprop  24705  spthonprp  24713  3oalem1  26706  elorrvc  28577  ballotlemfc0  28606  ballotlemfcc  28607  ballotlemodife  28611  ballotth  28651  wl-ax11-lem3  30189  mblfinlem1  30213  ovoliunnfl  30218  voliunnfl  30220  itg2addnclem2  30229  areacirclem5  30273  opnrebl2  30301  syldanl  30364  seqpo  30402  incsequz  30403  incsequz2  30404  ismtycnv  30460  prnc  30626  fperiodmullem  31664  climsuselem1  31774  climsuse  31775  0ellimcdiv  31816  fperdvper  31876  iblsplit  31926  stirlinglem11  32027  2reu1  32352  pfxsuff1eqwrdeq  32483  c0rnghm  32821  bj-eldiag2  34708  dihatexv2  37167
  Copyright terms: Public domain W3C validator