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  5950  funsnfsupp  9295  discld  23033  cncfcdm  24847  itgfsum  25784  dchreq  27225  lgsneg  27288  lgsquadlem2  27348  z12bdaylem1  28466  dfconngr1  30263  cover2  37916  iscnrm3rlem6  49190  0funcglem  49328  0funcg2  49329  thincmon  49678  thincepi  49679
  Copyright terms: Public domain W3C validator