Theorem pm5.32da 456

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 454	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

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:  rexbida  2545  reubida  2734  rmobida  2740  mpteq12f  4211  reuhypd  4617  funbrfv2b  5747  dffn5im  5748  eqfnfv2  5807  fndmin  5816  fniniseg  5829  fmptco  5874  dff13  5974  riotabidva  6056  mpoeq123dva  6149  mpoeq3dva  6152  suppssrst  6501  suppssrgst  6502  mpoxopovel  6512  qliftfun  6891  erovlem  6901  mapsnend  7099  xpcomco  7124  pw2f1odclem  7134  elfi2  7306  ctssdccl  7452  ltexpi  7705  dfplpq2  7722  axprecex  8248  zrevaddcl  9700  qrevaddcl  10054  icoshft  10403  fznn  10507  sseqn  11294  pfxeq  11483  pfxsuffeqwrdeq  11485  pfxsuff1eqwrdeq  11486  shftdm  11602  2shfti  11611  sumeq2  12143  fsum3  12172  fsum2dlemstep  12219  prodeq2  12342  fprodseq  12368  bitsmod  12741  bitscmp  12743  gcdaddm  12779  grpidpropdg  13745  ismgmid  13748  mhmpropd  13824  issubm2  13831  eqgid  14080  eqgabl  14185  rngpropd  14305  iscrng2  14370  ringpropd  14394  crngpropd  14395  crngunit  14469  dvdsrpropdg  14505  issubrg3  14606  lsslss  14769  lsspropdg  14819  znleval  15039  bastop2  15237  restopn2  15336  iscnp3  15356  lmbr2  15367  txlm  15432  ismet2  15507  xblpnfps  15551  xblpnf  15552  blininf  15577  blres  15587  elmopn2  15602  neibl  15644  metrest  15659  metcnp3  15664  metcnp  15665  metcnp2  15666  metcn  15667  txmetcn  15672  cnbl0  15687  cnblcld  15688  bl2ioo  15703  elcncf2  15727  cncfmet  15745  cnlimc  15825  lgsquadlem1  16318  lgsquadlem2  16319  2lgslem1a  16329  upgriswlkdc  16723  isclwwlknx  16779  clwwlkn1  16781  clwwlkn2  16784  eupth2lemsfi  16841