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

Theorem bibi12d 235
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 233 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 232 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 188 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm5.32  453  bi2bian9  608  cleqh  2277  abbi  2291  cleqf  2344  cbvreuvw  2709  vtoclb  2794  vtoclbg  2798  ceqsexg  2865  elabgf  2879  reu6  2926  ru  2961  sbcbig  3009  sbcne12g  3075  sbcnestgf  3108  preq12bg  3771  nalset  4130  undifexmid  4190  exmidsssn  4199  exmidsssnc  4200  exmidundif  4203  opthg  4234  opelopabsb  4256  wetriext  4572  opeliunxp2  4762  resieq  4912  elimasng  4991  cbviota  5178  iota2df  5197  fnbrfvb  5551  fvelimab  5567  fmptco  5677  fsng  5684  fressnfv  5698  funfvima3  5744  isorel  5802  isocnv  5805  isocnv2  5806  isotr  5810  ovg  6006  caovcang  6029  caovordg  6035  caovord3d  6038  caovord  6039  opeliunxp2f  6232  dftpos4  6257  ecopovsym  6624  ecopovsymg  6627  xpf1o  6837  nneneq  6850  supmoti  6985  supsnti  6997  isotilem  6998  isoti  6999  ltanqg  7377  ltmnqg  7378  elinp  7451  prnmaxl  7465  prnminu  7466  ltasrg  7747  axpre-ltadd  7863  zextle  9320  zextlt  9321  xlesubadd  9857  rexfiuz  10969  climshft  11283  dvdsext  11831  ltoddhalfle  11868  halfleoddlt  11869  bezoutlemmo  11977  bezoutlemeu  11978  bezoutlemle  11979  bezoutlemsup  11980  dfgcd3  11981  dvdssq  12002  rpexp  12123  pcdvdsb  12289  xmeteq0  13492  comet  13632  dedekindeulemuub  13728  dedekindeulemloc  13730  dedekindicclemuub  13737  dedekindicclemloc  13739  logltb  13928  bj-nalset  14269  bj-d0clsepcl  14299  bj-nn0sucALT  14352
  Copyright terms: Public domain W3C validator