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

Theorem bibi12d 234
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1 (𝜑 → (𝜓𝜒))
imbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
bibi12d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))

Proof of Theorem bibi12d
StepHypRef Expression
1 imbi12d.1 . . 3 (𝜑 → (𝜓𝜒))
21bibi1d 232 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 231 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 187 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.32  448  bi2bian9  582  cleqh  2217  abbi  2231  cleqf  2282  vtoclb  2717  vtoclbg  2721  ceqsexg  2787  elabgf  2800  reu6  2846  ru  2881  sbcbig  2927  sbcne12g  2991  sbcnestgf  3021  preq12bg  3670  nalset  4028  undifexmid  4087  exmidsssn  4095  exmidsssnc  4096  exmidundif  4099  opthg  4130  opelopabsb  4152  wetriext  4461  opeliunxp2  4649  resieq  4799  elimasng  4877  cbviota  5063  iota2df  5082  fnbrfvb  5430  fvelimab  5445  fmptco  5554  fsng  5561  fressnfv  5575  funfvima3  5619  isorel  5677  isocnv  5680  isocnv2  5681  isotr  5685  ovg  5877  caovcang  5900  caovordg  5906  caovord3d  5909  caovord  5910  opeliunxp2f  6103  dftpos4  6128  ecopovsym  6493  ecopovsymg  6496  xpf1o  6706  nneneq  6719  supmoti  6848  supsnti  6860  isotilem  6861  isoti  6862  ltanqg  7176  ltmnqg  7177  elinp  7250  prnmaxl  7264  prnminu  7265  ltasrg  7546  axpre-ltadd  7662  zextle  9110  zextlt  9111  xlesubadd  9634  rexfiuz  10729  climshft  11041  dvdsext  11480  ltoddhalfle  11517  halfleoddlt  11518  bezoutlemmo  11621  bezoutlemeu  11622  bezoutlemle  11623  bezoutlemsup  11624  dfgcd3  11625  dvdssq  11646  rpexp  11758  xmeteq0  12455  comet  12595  dedekindeulemuub  12691  dedekindeulemloc  12693  dedekindicclemuub  12700  dedekindicclemloc  12702  bj-nalset  13020  bj-d0clsepcl  13050  bj-nn0sucALT  13103
  Copyright terms: Public domain W3C validator