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

Theorem impbid1 140
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 127 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  impbid2  141  iba  294  ibar  295  pm4.81dc  852  pm5.63dc  892  pm4.83dc  897  pm5.71dc  907  19.33b2  1565  19.9t  1578  sb4b  1762  a16gb  1793  euor2  2006  eupickbi  2030  ceqsalg  2647  eqvincg  2739  ddifstab  3130  csbprc  3325  undif4  3342  eqifdc  3421  sssnm  3593  sneqbg  3602  opthpr  3611  elpwuni  3810  exmid01  4023  exmidundif  4026  eusv2i  4268  reusv3  4273  iunpw  4292  suc11g  4363  xpid11m  4646  ssxpbm  4853  ssxp1  4854  ssxp2  4855  xp11m  4856  2elresin  5111  mpteqb  5377  f1fveq  5533  f1elima  5534  f1imass  5535  fliftf  5560  nnsucuniel  6238  iserd  6298  ecopovtrn  6369  ecopover  6370  ecopovtrng  6372  ecopoverg  6373  map0g  6425  fopwdom  6532  f1finf1o  6635  addcanpig  6872  mulcanpig  6873  srpospr  7307  readdcan  7601  cnegexlem1  7636  addcan  7641  addcan2  7642  neg11  7712  negreb  7726  add20  7931  cru  8055  mulcanapd  8104  uz11  9010  eqreznegel  9068  lbzbi  9070  xneg11  9265  elioc2  9323  elico2  9324  elicc2  9325  fzopth  9443  2ffzeq  9517  flqidz  9658  addmodlteq  9770  frec2uzrand  9777  expcan  10090  nn0opthd  10095  fz1eqb  10164  cj11  10304  sqrt0  10402  recan  10507  0dvds  10898  dvds1  10936  alzdvds  10937  nn0enne  10984  nn0oddm1d2  10991  nnoddm1d2  10992  divalgmod  11009  gcdeq0  11050  algcvgblem  11113  prmexpb  11212  bj-peano4  11496  bj-nn0sucALT  11519
  Copyright terms: Public domain W3C validator