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

Theorem anbi1d 438
Description: Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
Hypothesis
Ref Expression
anbid.1 (φ → (ψχ))
Assertion
Ref Expression
anbi1d (φ → ((ψ θ) ↔ (χ θ)))

Proof of Theorem anbi1d
StepHypRef Expression
1 anbid.1 . . 3 (φ → (ψχ))
21a1d 22 . 2 (φ → (θ → (ψχ)))
32pm5.32rd 424 1 (φ → ((ψ θ) ↔ (χ θ)))
Colors of variables: wff set class
Syntax hints:  wi 4   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:  anbi1  439  anbi12d  442  bi2anan9  523  pm5.71dc  852  xorbi1d  1254  drsb1  1656  ax11ev  1685  eleq1  2076  rexeqf  2474  reueq1f  2475  rmoeq1f  2476  rabeqf  2522  vtocl2gaf  2591  alexeq  2641  ceqex  2642  elrabi  2666  sbc5  2758  rexss  2978  psstr  3020  sspsstr  3021  ineq1  3102  difin2  3170  r19.28m  3282  preq12bg  3510  opeq1  3515  eluni  3549  mpteq12f  3803  axsep2  3842  zfauscl  3843  opthg  3941  copsexg  3947  euotd  3957  elopab  3961  pocl  4006  uniuni  4124  rabxfrd  4142  regexmidlemm  4192  regexmidlem1  4193  preleq  4208  xpeq1  4277  elxpi  4279  vtoclr  4306  opbrop  4337  opelresg  4537  resopab2  4573  elxp4  4726  elxp5  4727  cnvpom  4778  fun11  4883  feq2  4948  f1eq2  5004  f1eq3  5005  foeq2  5019  brprcneu  5087  ssimaexg  5151  dmfco  5157  fndmdif  5188  rexsupp  5207  respreima  5211  isoeq5  5361  isoini  5373  isopolem  5377  f1oiso  5381  f1oiso2  5382  riotaeqdv  5385  acexmidlemab  5421  acexmidlemcase  5422  oprabid  5452  mpt2eq123  5478  mpt2eq123dva  5480  eloprabga  5505  resoprab  5511  resoprab2  5512  ov  5534  ovi3  5551  ov6g  5552  ovg  5553  caoftrn  5650  opabex3d  5662  opabex3  5663  elxp7  5711  eloprabi  5736  cnvf1o  5760  xporderlem  5765  poxp  5766  smoel2  5831  frec0g  5893  frecsuclem3  5897  frecsuc  5898  nnaordex  6002  qliftel  6088  brecop  6098  eroveu  6099  ecopovtrn  6105  ecopovtrng  6108  th3qlem2  6111  th3q  6113  dfplpq2  6202  dfmpq2  6203  ltsonq  6246  enq0sym  6276  enq0ref  6277  enq0tr  6278  enq0breq  6280  addnq0mo  6291  mulnq0mo  6292  addnnnq0  6293  mulnnnq0  6294  elinp  6317  prnmaxl  6331  prnminu  6332  prarloclemlo  6337  prarloc  6346  genpdflem  6350  genpassl  6368  genpassu  6369  ltexprlemm  6426  recexprlemell  6446  recexprlemelu  6447  addsrmo  6484  mulsrmo  6485  addsrpr  6486  mulsrpr  6487  lttrsr  6503  mulgt0sr  6517  ltresr  6548  axpre-lttrn  6576  axpre-mulgt0  6579  recexgt0  7170  apreap  7177  apreim  7193  prime  7905  ltxr  8174  ixxval  8244  bdsep2  8462  bdzfauscl  8466  bj-d0clsepcl  8502
  Copyright terms: Public domain W3C validator