Theorem biimparc 419

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 156	. 2 |- (ch -> (ph -> ps))
3	2	imp 350	1 |- ((ch /\ ph) -> ps)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  biantr 741  elpw2g 2722  elon2 2954  ideqg 3271  eqfnfv 3788  elunirnALT 3860  dom2d 4391  mapxpen 4481  mapunen 4488  ssnn 4520  unfilem1 4530  iunfi 4549  inf3lem2 4594  aceq5lem5 4719  aceq6b 4722  indpi 5014  ltexprlem6 5127  prlem936 5135  expnbndt 6593  climsup 7099  caucvg3t 7112  unbenlem 7455  infmap2lem2 7530  spanunsn 9442  nonbool 9536  nmopunt 9877  lncnopbd 9904  pjnmop 10013  sumdmdlem 10281  findabrcl 10352

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