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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biantru  302  biantrud  304  ancrb  322  rbaibd  936  dedlem0a  981  fvopab6  5808  fressnfv  5905  tpostpos  6539  nnmword  6795  unfiexmid  7230  ltmpig  7713  mul0eqap  9009  sup3exmid  9296  xrmaxiflemcom  12041  rexrals  17369  rexals  17375