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 742  elpw2g 2727  elon2 2959  ideqg 3276  eqfnfv 3797  elunirnALT 3869  dom2d 4404  mapxpen 4495  mapunen 4502  ssnnfi 4535  ssnnfiOLD 4536  unfilem1 4548  iunfiOLD 4569  inf3lem2 4614  aceq5lem5 4739  aceq6b 4742  indpi 5034  ltexprlem6 5147  prlem936 5155  expnbndt 6654  climsup 7155  caucvg3t 7168  unbenlem 7504  infmap2lem2 7580  spanunsn 9502  nonbool 9596  nmopunt 9939  lncnopbd 9966  pjnmop 10075  sumdmdlem 10345  findabrcl 10418

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