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

Theorem anbi1d 441
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 427 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  442  anbi12d  445  bi2anan9  526  pm5.71dc  856  xorbi1d  1256  drsb1  1662  ax11ev  1691  eleq1  2082  rexeqf  2480  reueq1f  2481  rmoeq1f  2482  rabeqf  2528  vtocl2gaf  2597  alexeq  2647  ceqex  2648  elrabi  2672  sbc5  2764  rexss  2984  psstr  3026  sspsstr  3027  ineq1  3108  difin2  3176  r19.28m  3288  preq12bg  3518  opeq1  3523  eluni  3557  mpteq12f  3811  axsep2  3850  zfauscl  3851  opthg  3949  copsexg  3955  euotd  3965  elopab  3969  pocl  4014  uniuni  4133  rabxfrd  4151  regexmidlemm  4201  regexmidlem1  4202  preleq  4217  xpeq1  4286  elxpi  4288  vtoclr  4315  opbrop  4346  opelresg  4546  resopab2  4582  elxp4  4735  elxp5  4736  cnvpom  4787  fun11  4892  feq2  4957  f1eq2  5013  f1eq3  5014  foeq2  5028  brprcneu  5096  ssimaexg  5160  dmfco  5166  fndmdif  5197  rexsupp  5216  respreima  5220  isoeq5  5370  isoini  5382  isopolem  5386  f1oiso  5390  f1oiso2  5391  riotaeqdv  5394  acexmidlemab  5430  acexmidlemcase  5431  oprabid  5461  mpt2eq123  5487  mpt2eq123dva  5489  eloprabga  5514  resoprab  5520  resoprab2  5521  ov  5543  ovi3  5560  ov6g  5561  ovg  5562  caoftrn  5659  opabex3d  5671  opabex3  5672  elxp7  5720  eloprabi  5745  cnvf1o  5769  xporderlem  5774  poxp  5775  smoel2  5840  frec0g  5902  frecsuclem3  5906  frecsuc  5907  nnaordex  6011  qliftel  6097  brecop  6107  eroveu  6108  ecopovtrn  6114  ecopovtrng  6117  th3qlem2  6120  th3q  6122  dfplpq2  6213  dfmpq2  6214  ltsonq  6257  enq0sym  6287  enq0ref  6288  enq0tr  6289  enq0breq  6291  addnq0mo  6302  mulnq0mo  6303  addnnnq0  6304  mulnnnq0  6305  elinp  6328  prnmaxl  6342  prnminu  6343  prarloclemlo  6348  prarloc  6357  genpdflem  6361  genpassl  6379  genpassu  6380  ltexprlemm  6437  recexprlemell  6456  recexprlemelu  6457  addsrmo  6490  mulsrmo  6491  addsrpr  6492  mulsrpr  6493  lttrsr  6509  mulgt0sr  6522  ltresr  6550  axpre-lttrn  6578  axpre-mulgt0  6580  bdsep2  7112  bdzfauscl  7116  bj-d0clsepcl  7148
  Copyright terms: Public domain W3C validator