New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpbiran2 GIF version

Theorem mpbiran2 885
 Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
Hypotheses
Ref Expression
mpbiran2.1 χ
mpbiran2.2 (φ ↔ (ψ χ))
Assertion
Ref Expression
mpbiran2 (φψ)

Proof of Theorem mpbiran2
StepHypRef Expression
1 mpbiran2.2 . 2 (φ ↔ (ψ χ))
2 mpbiran2.1 . . 3 χ
32biantru 491 . 2 (ψ ↔ (ψ χ))
41, 3bitr4i 243 1 (φψ)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358 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 177  df-an 360 This theorem is referenced by:  pm5.62  889  reueq  3033  ss0b  3580  dfimak2  4298  dfpw2  4327  ltfinex  4464  ssfin  4470  eqpw1relk  4479  ncfinraiselem2  4480  eqtfinrelk  4486  evenodddisjlem1  4515  nnadjoinlem1  4519  tfinnnlem1  4533  dfphi2  4569  dfop2lem1  4573  setconslem2  4732  setconslem4  4734  f1funfun  5263  fores  5278  funfv  5375  otelins3  5792  releqmpt  5808  releqmpt2  5809  fnsex  5832  foundex  5914  enmap2lem1  6063  enmap1lem1  6069  fnce  6176  sbthlem1  6203  sbthlem3  6205  tcfnex  6244  nncdiv3lem2  6276  nchoicelem9  6297  nchoicelem11  6299
 Copyright terms: Public domain W3C validator