Theorem pm5.32i 449

Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)

Hypothesis

Ref	Expression
pm5.32i.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
pm5.32i	⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

Proof of Theorem pm5.32i

Step	Hyp	Ref	Expression
1		pm5.32i.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		pm5.32 448	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
3	1, 2	mpbi 144	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.32ri  450  biadan2  451  anbi2i  452  abai  549  anabs5  562  pm5.33  598  eq2tri  2197  rexbiia  2448  reubiia  2613  rmobiia  2618  rabbiia  2666  ceqsrexbv  2811  euxfrdc  2865  eldifsn  3645  elrint  3806  elriin  3878  opeqsn  4169  rabxp  4571  eliunxp  4673  ressn  5074  fncnv  5184  dff1o5  5369  respreima  5541  dff4im  5559  dffo3  5560  f1ompt  5564  fsn  5585  fconst3m  5632  fconst4m  5633  eufnfv  5641  dff13  5662  f1mpt  5665  isores2  5707  isoini  5712  eloprabga  5851  mpomptx  5855  resoprab  5860  ov6g  5901  dfopab2  6080  dfoprab3s  6081  dfoprab3  6082  f1od2  6125  brtpos2  6141  dftpos3  6152  tpostpos  6154  dfsmo2  6177  elixp2  6589  mapsnen  6698  xpcomco  6713  eqinfti  6900  dfplpq2  7155  dfmpq2  7156  enq0enq  7232  nqnq0a  7255  nqnq0m  7256  genpassl  7325  genpassu  7326  axsuploc  7830  recexre  8333  recexgt0  8335  reapmul1  8350  apsqgt0  8356  apreim  8358  recexaplem2  8406  rerecclap  8483  elznn0  9062  elznn  9063  msqznn  9144  eluz2b1  9388  eluz2b3  9391  qreccl  9427  rpnegap  9467  elfz2nn0  9885  elfzo3  9933  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  qexpclz  10307  shftidt2  10597  clim0  11047  iser3shft  11108  summodclem3  11142  eftlub  11385  ndvdsadd  11617  algfx  11722  isprm3  11788  ssntr  12280  tx1cn  12427  tx2cn  12428  pilem1  12849