Theorem biimpar 325

Description: Inference from a logical equivalence.

Hypothesis

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

Assertion

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

Proof of Theorem biimpar

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

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

This theorem is referenced by:  oplem1 578  cleqtr 1118  opabss 2100  sotrieq 2149  relss 2480  funfni 2724  fnssres 2734  f1ores 2813  f1oco 2816  fvopab3ig 2869  abrexexlem1 2910  isomin 2937  tfrlem1 2949  tfr3 2964  oprabvalig 3048  oawordri 3152  oaass 3163  en3d 3304  aceq5 3563  ltexprlem7 3942  uzind 4603  cvexchlem 5759

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