Theorem iba 300

Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) (Revised by NM, 24-Mar-2013.)

Assertion

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

Proof of Theorem iba

Step	Hyp	Ref	Expression
1		pm3.21 264	. 2 |- ( ph -> ( ps -> ( ps /\ ph ) ) )
2		simpl 109	. 2 |- ( ( ps /\ ph ) -> ps )
3	1, 2	impbid1 142	1 |- ( ph -> ( ps <-> ( ps /\ ph ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biantru  302  biantrud  304  ancrb  322  rbaibd  936  dedlem0a  981  fvopab6  5799  fressnfv  5896  tpostpos  6529  nnmword  6785  unfiexmid  7219  ltmpig  7700  mul0eqap  8994  sup3exmid  9281  xrmaxiflemcom  11998  rexrals  17124  rexals  17130