Theorem pm5.32i 454

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 453	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
3	1, 2	mpbi 145	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

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:  pm5.32ri  455  biadan2  456  anbi2i  457  abai  560  anabs5  573  pm5.33  609  eq2tri  2237  rexbiia  2492  reubiia  2661  rmobiia  2666  rabbiia  2722  ceqsrexbv  2868  euxfrdc  2923  eldifpr  3619  eldiftp  3638  eldifsn  3719  elrint  3884  elriin  3957  opeqsn  4252  rabxp  4663  eliunxp  4766  restidsing  4963  ressn  5169  fncnv  5282  dff1o5  5470  respreima  5644  dff4im  5662  dffo3  5663  f1ompt  5667  fsn  5688  fconst3m  5735  fconst4m  5736  eufnfv  5747  dff13  5768  f1mpt  5771  isores2  5813  isoini  5818  eloprabga  5961  mpomptx  5965  resoprab  5970  ov6g  6011  dfopab2  6189  dfoprab3s  6190  dfoprab3  6191  f1od2  6235  brtpos2  6251  dftpos3  6262  tpostpos  6264  dfsmo2  6287  elixp2  6701  mapsnen  6810  xpcomco  6825  eqinfti  7018  dfplpq2  7352  dfmpq2  7353  enq0enq  7429  nqnq0a  7452  nqnq0m  7453  genpassl  7522  genpassu  7523  axsuploc  8029  recexre  8534  recexgt0  8536  reapmul1  8551  apsqgt0  8557  apreim  8559  recexaplem2  8608  rerecclap  8686  elznn0  9267  elznn  9268  msqznn  9352  eluz2b1  9600  eluz2b3  9603  qreccl  9641  rpnegap  9685  elfz2nn0  10111  elfzo3  10162  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  qexpclz  10540  shftidt2  10840  clim0  11292  iser3shft  11353  summodclem3  11387  fprod2dlemstep  11629  eftlub  11697  ndvdsadd  11935  algfx  12051  isprm3  12117  isprm5  12141  xpsfrnel  12762  isabl2  13095  dvdsrcl2  13266  unitinvcl  13290  unitinvinv  13291  unitlinv  13293  unitrinv  13294  ssntr  13558  tx1cn  13705  tx2cn  13706  pilem1  14136  lgsdir2lem4  14368