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

Theorem anbi2d 452
Description: Deduction adding a left 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
anbi2d (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))

Proof of Theorem anbi2d
StepHypRef Expression
1 anbid.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 22 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32pm5.32d 438 1 (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  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:  anbi2  455  anbi12d  457  bi2anan9  571  dn1dc  902  xorbi2d  1312  dfbi3dc  1329  xordidc  1331  eleq2  2143  ceqsex2  2640  ceqsex6v  2644  vtocl2gaf  2666  ceqsrex2v  2728  mob2  2773  eqreu  2785  nelrdva  2798  undif4  3313  r19.27m  3344  ifbi  3377  preq12bg  3573  opeq2  3579  ralunsn  3597  intab  3673  opabbid  3851  opthg  4001  pocl  4066  ordelord  4144  ordtriexmid  4273  ontr2exmid  4276  onsucsssucexmid  4278  tfisi  4336  xpeq2  4386  rabxp  4406  vtoclr  4414  opeliunxp  4421  posng  4438  opbrop  4445  rexiunxp  4506  elrnmpt1  4613  dfres2  4688  brcodir  4742  poltletr  4755  xp11m  4789  elxp4  4838  elxp5  4839  dffun4f  4948  fununi  4998  fneq2  5019  fnun  5036  feq3  5063  foeq3  5135  funfveu  5219  funbrfv  5244  ssimaexg  5267  fvopab3g  5277  fvopab3ig  5278  fvelrn  5330  fmptco  5362  fsn2  5369  elunirn  5437  isoeq2  5473  isoeq3  5474  isocnv2  5483  isoini  5488  isopolem  5492  f1oiso  5496  f1oiso2  5497  oprabbid  5589  cbvoprab3  5611  mpt2mptx  5626  mpt2fun  5634  ov  5651  ovi3  5668  ov6g  5669  ovg  5670  caoftrn  5767  f1o2ndf1  5880  xporderlem  5883  f1od2  5887  brtpos2  5900  brtposg  5903  dftpos4  5912  recseq  5955  tfrlem3-2d  5961  tfrlemi1  5981  tfrexlem  5983  tfr1onlemaccex  5997  tfrcllemaccex  6010  tfrcl  6013  freceq1  6041  freceq2  6042  frecsuc  6056  nnaordex  6166  brecop  6262  eroveu  6263  erovlem  6264  ecopovtrn  6269  ecopovtrng  6272  th3qlem1  6274  th3qlem2  6275  th3q  6277  domeng  6299  dom2lem  6319  xpcomco  6370  xpassen  6374  xpdom2  6375  xpf1o  6385  phplem3g  6391  ssfiexmid  6411  domfiexmid  6413  findcard2  6423  findcard2s  6424  findcard2d  6425  findcard2sd  6426  diffifi  6428  supeq2  6461  recexnq  6642  recmulnqg  6643  ltsonq  6650  enq0sym  6684  enq0ref  6685  enq0tr  6686  enq0breq  6688  addnq0mo  6699  mulnq0mo  6700  addnnnq0  6701  mulnnnq0  6702  elinp  6726  prdisj  6744  prarloclem3  6749  prarloc  6755  distrlem5prl  6838  distrlem5pru  6839  ltexprlemell  6850  ltexprlemelu  6851  recexprlemm  6876  addsrmo  6982  mulsrmo  6983  addsrpr  6984  mulsrpr  6985  lttrsr  7001  recexgt0sr  7012  mulgt0sr  7016  ltresr  7069  axprecex  7108  axpre-lttrn  7112  axpre-mulgt0  7115  lesub0  7650  apreap  7754  apreim  7770  zltlen  8507  prime  8527  fzind  8543  qltlen  8806  xltnegi  8978  ixxval  8995  fzval  9107  fzdifsuc  9174  elfzm11  9184  elfzo  9236  exbtwnzlemshrink  9335  rebtwn2zlemshrink  9340  facwordi  9764  shftfvalg  9844  shftfibg  9846  shftfval  9847  shftfib  9849  shftfn  9850  2shfti  9857  cau3lem  10138  caubnd2  10141  clim  10258  clim2  10260  climi  10264  climcn2  10286  addcn2  10287  subcn2  10288  mulcn2  10289  divalgb  10469  ndvdssub  10474  zsupcllemex  10486  gcdval  10495  gcdneg  10517  bezoutlemstep  10530  bezoutlemmain  10531  bezoutlemex  10534  dfgcd2  10547  gcdass  10548  algcvgblem  10575  lcmval  10589  lcmneg  10600  lcmgcdlem  10603  lcmass  10611  qredeq  10622  prmind2  10646  euclemma  10669  pw2dvdslemn  10687  qnumval  10707  qdenval  10708
  Copyright terms: Public domain W3C validator