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

Theorem mpbiran2d 708
Description: Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.)
Hypotheses
Ref Expression
mpbiran2d.1 (𝜑𝜃)
mpbiran2d.2 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
Assertion
Ref Expression
mpbiran2d (𝜑 → (𝜓𝜒))

Proof of Theorem mpbiran2d
StepHypRef Expression
1 mpbiran2d.1 . 2 (𝜑𝜃)
2 mpbiran2d.2 . . 3 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
32biancomd 463 . 2 (𝜑 → (𝜓 ↔ (𝜃𝜒)))
41, 3mpbirand 707 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  opelidres  6009  funsnfsupp  9432  discld  23097  cncfcdm  24924  itgfsum  25862  dchreq  27302  lgsneg  27365  lgsquadlem2  27425  dfconngr1  30207  cover2  37722  iscnrm3rlem6  48842  0funcglem  48916  0funcg2  48917  thincmon  49082  thincepi  49083
  Copyright terms: Public domain W3C validator