ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  impbid1 Structured version   GIF version

Theorem impbid1 130
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 9 . 2 (φ → (χψ))
41, 3impbid 120 1 (φ → (ψχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  impbid2  131  iba  284  ibar  285  pm4.81dc  807  pm5.63dc  841  pm4.83dc  846  pm5.71dc  856  19.33b2  1502  19.9t  1515  sb4b  1697  a16gb  1727  euor2  1940  eupickbi  1964  ceqsalg  2559  eqvincg  2645  csbprc  3239  undif4  3261  sssnm  3499  sneqbg  3508  opthpr  3517  elpwuni  3715  eusv2i  4137  reusv3  4142  iunpw  4161  suc11g  4219  xpid11m  4484  ssxpbm  4683  ssxp1  4684  ssxp2  4685  xp11m  4686  2elresin  4936  mpteqb  5186  f1fveq  5336  f1elima  5337  f1imass  5338  fliftf  5364  iserd  6043  ecopovtrn  6114  ecopover  6115  ecopovtrng  6117  ecopoverg  6118  addcanpig  6194  mulcanpig  6195  readdcan  6746  cnegexlem1  6779  addcan  6784  addcan2  6785  neg11  6854  negreb  6868  bj-peano4  7324  bj-nn0sucALT  7343
  Copyright terms: Public domain W3C validator