Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.74da Structured version   Visualization version   GIF version

Theorem pm5.74da 723
 Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 4-May-2007.)
Hypothesis
Ref Expression
pm5.74da.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
pm5.74da (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))

Proof of Theorem pm5.74da
StepHypRef Expression
1 pm5.74da.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 449 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32pm5.74d 262 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197  df-an 385 This theorem is referenced by:  ralbida  3011  ralbidva  3014  ralxpxfr2d  3358  elrab3t  3395  ordunisuc2  7086  dfom2  7109  pwfseqlem3  9520  lo1resb  14339  rlimresb  14340  o1resb  14341  fsumparts  14582  isprm3  15443  ramval  15759  islindf4  20225  cnntr  21127  fclsbas  21872  metcnp  22393  voliunlem3  23366  ellimc2  23686  limcflf  23690  mdegleb  23869  xrlimcnp  24740  dchrelbas3  25008  lmicom  25725  dmdbr5ati  29409  vtocl2d  29442  isarchi3  29869  cmpcref  30045  sscoid  32145  cdlemefrs29bpre0  36001  cdlemkid3N  36538  cdlemkid4  36539  hdmap1eulem  37430  hdmap1eulemOLDN  37431  jm2.25  37883  ntrneik2  38707  ntrneix2  38708  ntrneikb  38709  fourierdlem87  40728
 Copyright terms: Public domain W3C validator