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

Theorem anbi12i 436
Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
anbi12.1 (φψ)
anbi12.2 (χθ)
Assertion
Ref Expression
anbi12i ((φ χ) ↔ (ψ θ))

Proof of Theorem anbi12i
StepHypRef Expression
1 anbi12.1 . . 3 (φψ)
21anbi1i 434 . 2 ((φ χ) ↔ (ψ χ))
3 anbi12.2 . . 3 (χθ)
43anbi2i 433 . 2 ((ψ χ) ↔ (ψ θ))
52, 4bitri 173 1 ((φ χ) ↔ (ψ θ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  anbi12ci  437  ordir  718  orddi  721  dcan  830  3anbi123i  1079  an6  1201  xorcom  1262  trubifal  1290  truxortru  1293  truxorfal  1294  falxortru  1295  falxorfal  1296  nford  1441  nfand  1442  sbequ8  1709  sbanv  1751  sban  1811  sbbi  1815  sbnf2  1839  eu1  1907  2exeu  1974  2eu4  1975  sbabel  2185  neanior  2270  rexeqbii  2315  r19.26m  2422  reean  2456  reu5  2500  reu2  2706  reu3  2708  eqss  2937  unss  3094  ralunb  3101  ssin  3136  undi  3162  difundi  3166  indifdir  3170  inab  3182  difab  3183  reuss2  3194  reupick  3198  raaan  3306  prss  3494  tpss  3503  prsspw  3510  prneimg  3519  uniin  3574  intun  3620  intpr  3621  brin  3785  brdif  3786  ssext  3931  pweqb  3933  opthg2  3950  copsex4g  3958  opelopabsb  3971  eqopab2b  3990  pwin  3993  pofun  4023  elxp3  4321  soinxp  4337  relun  4381  inopab  4395  difopab  4396  inxp  4397  opelco2g  4430  cnvco  4447  dmin  4470  intasym  4636  asymref  4637  cnvdif  4657  xpm  4672  xp11m  4686  dfco2  4747  relssdmrn  4768  cnvpom  4787  xpcom  4791  dffun4  4840  dffun4f  4844  funun  4870  funcnveq  4888  fun11  4892  fununi  4893  imadif  4905  imainlem  4906  imain  4907  fnres  4941  fnopabg  4948  fun  4988  fin  5001  dff1o2  5056  brprcneu  5096  fsn  5260  dff1o6  5341  isotr  5381  brabvv  5474  eqoprab2b  5486  dfoprab3  5740  poxp  5775  brtpos2  5788  tfrlem7  5855  dfer2  6018  eqer  6049  iinerm  6089  brecop  6107  eroveu  6108  erovlem  6109  oviec  6123  dfmq0qs  6284  dfplq0qs  6285  enq0enq  6286  enq0tr  6289  npsspw  6325  nqprdisj  6399  ltexprlemdisj  6443  addcanprg  6453  recexprlemdisj  6464  addsrpr  6492  mulsrpr  6493  mulgt0sr  6522  addcnsr  6545  mulcnsr  6546  ltresr  6550  axcnre  6575
  Copyright terms: Public domain W3C validator