Theorem ibar 487

Description: Introduction of antecedent as conjunct.

Assertion

Ref	Expression
ibar	|- (ph -> (ps <-> (ph /\ ps)))

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		anclb 264	. 2 |- ((ph -> ps) <-> (ph -> (ph /\ ps)))
2	1	pm5.74ri 445	1 |- (ph -> (ps <-> (ph /\ ps)))

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

This theorem is referenced by:  baib 506  biantrur 544  ceqsrexv 1413  iunconst 2000  dfom2 2374  brinxp 2466  fvopab3 2868  oprabval 3047  brecop 3242  aceq3 3556  ltprord 3928  clim2 4881  hlim2 5112  cmbrt 5494  cvbrt 5714  mdbr 5726  chrelat 5757

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