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

Theorem anc2li 302
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 300 . 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 223
This theorem is referenced by:  imdistani 443  equvini 1151  pwpw0 2439  sssn 2443  opprc3 2764  tfis 3090  oeordi 4152  unblem3 4471  trcl 4569  rankr1 4598  ac5b 4677  sqr2irr 6610  metelcls 7848  h1datom 9635
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 147  df-an 225
Copyright terms: Public domain