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  813  pm5.63dc  852  pm4.83dc  857  pm5.71dc  867  19.33b2  1517  19.9t  1530  sb4b  1712  a16gb  1742  euor2  1955  eupickbi  1979  ceqsalg  2576  eqvincg  2662  csbprc  3256  undif4  3278  sssnm  3516  sneqbg  3525  opthpr  3534  elpwuni  3732  eusv2i  4153  reusv3  4158  iunpw  4177  suc11g  4235  xpid11m  4500  ssxpbm  4699  ssxp1  4700  ssxp2  4701  xp11m  4702  2elresin  4953  mpteqb  5204  f1fveq  5354  f1elima  5355  f1imass  5356  fliftf  5382  iserd  6068  ecopovtrn  6139  ecopover  6140  ecopovtrng  6142  ecopoverg  6143  fopwdom  6246  addcanpig  6318  mulcanpig  6319  readdcan  6930  cnegexlem1  6963  addcan  6968  addcan2  6969  neg11  7038  negreb  7052  add20  7244  cru  7366  mulcanapd  7404  uz11  8251  eqreznegel  8305  lbzbi  8307  xneg11  8497  elioc2  8555  elico2  8556  elicc2  8557  fzopth  8674  2ffzeq  8748  frec2uzrand  8852  cj11  9113  sqrt0  9193  bj-peano4  9389  bj-nn0sucALT  9408
  Copyright terms: Public domain W3C validator