HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem anc2li 324
Description: Deduction conjoining antecedent to left of consequent in nested implication.
Hypothesis
Ref Expression
anc2li.1 |- (ph -> (ps -> ch))
Assertion
Ref Expression
anc2li |- (ph -> (ps -> (ph /\ ch)))

Proof of Theorem anc2li
StepHypRef Expression
1 anc2li.1 . 2 |- (ph -> (ps -> ch))
2 anc2l 322 . 2 |- ((ph -> (ps -> ch)) -> (ph -> (ps -> (ph /\ ch))))
31, 2ax-mp 7 1 |- (ph -> (ps -> (ph /\ ch)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 239
This theorem is referenced by:  imdistani 489  equvini 1369  equviniOLD 1370  pwpw0 2956  sssn 2964  pwsnALT 2995  opprc3 3358  ordtr2 3523  tfis 3749  oeordi 5073  unblem3 5445  trcl 5561  rankr1 5594  ac5b 5711  sqr2irr 7774  metelcls 9038  h1datomi 10929  wfisg 13709  frinsg 13733  sbiota1 16081
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 163  df-an 241
Copyright terms: Public domain