Theorem pm5.32i 427

Description: Distribution of implication over biconditional (inference rule). (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 426	. 2 ⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
3	1, 2	mpbi 133	1 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm5.32ri  428  biadan2  429  anbi2i  430  abai  494  anabs5  507  pm5.33  541  eq2tri  2099  rexbiia  2339  reubiia  2494  rmobiia  2499  rabbiia  2547  ceqsrexbv  2675  euxfrdc  2727  dfpss3  3030  eldifsn  3495  elrint  3655  elriin  3727  opeqsn  3989  rabxp  4380  eliunxp  4475  ressn  4858  fncnv  4965  dff1o5  5135  respreima  5295  dff4im  5313  dffo3  5314  f1ompt  5320  fsn  5335  fconst3m  5380  fconst4m  5381  eufnfv  5389  dff13  5407  f1mpt  5410  isores2  5453  isoini  5457  eloprabga  5591  mpt2mptx  5595  resoprab  5597  ov6g  5638  dfopab2  5815  dfoprab3s  5816  dfoprab3  5817  brtpos2  5866  dftpos3  5877  tpostpos  5879  dfsmo2  5902  xpcomco  6300  dfplpq2  6452  dfmpq2  6453  enq0enq  6529  nqnq0a  6552  nqnq0m  6553  genpassl  6622  genpassu  6623  recexre  7569  recexgt0  7571  reapmul1  7586  apsqgt0  7592  apreim  7594  recexaplem2  7633  rerecclap  7706  elznn0  8260  elznn  8261  msqznn  8338  eluz2b1  8539  eluz2b3  8541  qreccl  8576  rpnegap  8615  elfz2nn0  8973  elfzo3  9019  frecuzrdgfn  9198  qexpclz  9276  shftidt2  9433  clim0  9806  ialgfx  9891