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

Theorem impbid1 194
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)
Hypotheses
Ref Expression
impbid1.1 (φ → (ψχ))
impbid1.2 (χψ)
Assertion
Ref Expression
impbid1 (φ → (ψχ))

Proof of Theorem impbid1
StepHypRef Expression
1 impbid1.1 . 2 (φ → (ψχ))
2 impbid1.2 . . 3 (χψ)
32a1i 10 . 2 (φ → (χψ))
41, 3impbid 183 1 (φ → (ψχ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176
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
This theorem is referenced by:  impbid2  195  iba  489  ibar  490  pm5.71  902  cad0  1400  19.33b  1608  19.9t  1779  19.9tOLD  1857  a16gb  2050  sb4b  2054  eupickbi  2270  euor2  2272  2eu1  2284  2eu3  2286  ceqsalg  2883  undif4  3607  sneqbg  3875  adj11  3889  elpwuni  4053  opkthg  4131  iotanul  4354  preaddccan2  4455  suc11nnc  4558  phialllem1  4616  ssxpb  5055  xp11  5056  xpcan  5057  xpcan2  5058  imadif  5171  2elresin  5194  f1fveq  5473  f1elima  5474  enpw1  6062  peano4nc  6150  addceq0  6219  ce0tb  6238  addccan2nc  6265
  Copyright terms: Public domain W3C validator