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

Theorem bibi12d 233
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 231 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 230 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 186 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-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.32  441  bi2bian9  575  cleqh  2187  abbi  2201  cleqf  2252  vtoclb  2676  vtoclbg  2680  ceqsexg  2743  elabgf  2756  reu6  2802  ru  2837  sbcbig  2883  sbcne12g  2947  sbcnestgf  2977  preq12bg  3612  nalset  3961  undifexmid  4019  exmidundif  4026  opthg  4056  opelopabsb  4078  wetriext  4382  opeliunxp2  4564  resieq  4711  elimasng  4787  cbviota  4972  iota2df  4991  fnbrfvb  5329  fvelimab  5344  fmptco  5448  fsng  5454  fressnfv  5468  funfvima3  5510  isorel  5569  isocnv  5572  isocnv2  5573  isotr  5577  ovg  5765  caovcang  5788  caovordg  5794  caovord3d  5797  caovord  5798  opeliunxp2f  5985  dftpos4  6010  ecopovsym  6368  ecopovsymg  6371  xpf1o  6540  nneneq  6553  supmoti  6667  supsnti  6679  isotilem  6680  isoti  6681  ltanqg  6938  ltmnqg  6939  elinp  7012  prnmaxl  7026  prnminu  7027  ltasrg  7295  axpre-ltadd  7400  zextle  8807  zextlt  8808  rexfiuz  10387  climshft  10656  dvdsext  10949  ltoddhalfle  10986  halfleoddlt  10987  bezoutlemmo  11088  bezoutlemeu  11089  bezoutlemle  11090  bezoutlemsup  11091  dfgcd3  11092  dvdssq  11113  rpexp  11225  bj-nalset  11443  bj-d0clsepcl  11477  bj-nn0sucALT  11530
  Copyright terms: Public domain W3C validator