Theorem pm5.32da 452

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)

Hypothesis

Ref	Expression
pm5.32da.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
pm5.32da	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Proof of Theorem pm5.32da

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 450	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:  rexbida  2525  reubida  2713  rmobida  2719  mpteq12f  4167  reuhypd  4566  funbrfv2b  5686  dffn5im  5687  eqfnfv2  5741  fndmin  5750  fniniseg  5763  rexsupp  5767  fmptco  5809  dff13  5904  riotabidva  5984  mpoeq123dva  6077  mpoeq3dva  6080  mpoxopovel  6402  qliftfun  6781  erovlem  6791  xpcomco  7005  pw2f1odclem  7015  elfi2  7165  ctssdccl  7304  ltexpi  7550  dfplpq2  7567  axprecex  8093  zrevaddcl  9523  qrevaddcl  9871  icoshft  10218  fznn  10317  pfxeq  11270  pfxsuffeqwrdeq  11272  pfxsuff1eqwrdeq  11273  shftdm  11376  2shfti  11385  sumeq2  11913  fsum3  11941  fsum2dlemstep  11988  prodeq2  12111  fprodseq  12137  bitsmod  12510  bitscmp  12512  gcdaddm  12548  grpidpropdg  13450  ismgmid  13453  gsumpropd2  13469  mhmpropd  13542  issubm2  13549  eqgid  13806  eqgabl  13910  rngpropd  13961  iscrng2  14021  ringpropd  14044  crngpropd  14045  crngunit  14118  dvdsrpropdg  14154  issubrg3  14254  lsslss  14388  lsspropdg  14438  znleval  14660  bastop2  14801  restopn2  14900  iscnp3  14920  lmbr2  14931  txlm  14996  ismet2  15071  xblpnfps  15115  xblpnf  15116  blininf  15141  blres  15151  elmopn2  15166  neibl  15208  metrest  15223  metcnp3  15228  metcnp  15229  metcnp2  15230  metcn  15231  txmetcn  15236  cnbl0  15251  cnblcld  15252  bl2ioo  15267  elcncf2  15291  cncfmet  15309  cnlimc  15389  lgsquadlem1  15799  lgsquadlem2  15800  2lgslem1a  15810  upgriswlkdc  16171  isclwwlknx  16225  clwwlkn1  16227  clwwlkn2  16230