Theorem biimpac 418

Description: Inference from a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem biimpac

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpcd 155	. 2 |- (ps -> (ph -> ch))
3	2	imp 350	1 |- ((ps /\ ph) -> ch)

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

This theorem is referenced by:  gencbvex2 1830  sseq0 2294  ordnbtwn 3053  onsucuni2 3081  eqop 4088  omlimcl 4193  fodomr 4463  xpmapenlem4 4479  fodomfib 4541  aceq5lem4 4710  aceq5 4712  fodomb 4772  alephval3 4875  ltrpq 5057  map2psrpr 5192  eqlet 5544  addge0 5573  metxp 7774  cncms 7932  hhcms 8993  hhsscms 9067  spansncv 9514  eigpos 9679  pjnormss 10007  sumdmdlem 10252

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