Theorem biimparc 327

Description: Inference from a logical equivalence.

Hypothesis

Ref	Expression
biimpa.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
biimparc	|- ((ch /\ ph) -> ps)

Proof of Theorem biimparc

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimprcd 138	. 2 |- (ch -> (ph -> ps))
3	2	imp 277	1 |- ((ch /\ ph) -> ps)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  biantr 556  eueq 1427  elon2 2210  funsn 2690  cleqfv 2880  dom2d 3307  mapxpen 3390  mapunen 3397  ssnn 3429  unfilem1 3438  inf3lem2 3465  aceq5lem5 3562  aceq6b 3565  indpi 3828  ltexprlem6 3941  prlem936 3949  negeu 4124  receu 4215  infmap2lem2 4952  spanunsn 5482  5oalem4 5547  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org