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

Theorem bitr3d 183
 Description: Deduction form of bitr3i 179. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3d.1 (𝜑 → (𝜓𝜒))
bitr3d.2 (𝜑 → (𝜓𝜃))
Assertion
Ref Expression
bitr3d (𝜑 → (𝜒𝜃))

Proof of Theorem bitr3d
StepHypRef Expression
1 bitr3d.1 . . 3 (𝜑 → (𝜓𝜒))
21bicomd 133 . 2 (𝜑 → (𝜒𝜓))
3 bitr3d.2 . 2 (𝜑 → (𝜓𝜃))
42, 3bitrd 181 1 (𝜑 → (𝜒𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  3bitrrd  208  3bitr3d  211  3bitr3rd  212  pm5.16  748  biassdc  1302  pm5.24dc  1305  anxordi  1307  sbequ12a  1672  drex1  1695  sbcomxyyz  1862  sb9v  1870  csbiebt  2914  prsspwg  3551  bnd2  3954  copsex2t  4010  copsex2g  4011  fnssresb  5039  fcnvres  5101  dmfco  5269  funimass5  5312  fmptco  5358  cbvfo  5453  cbvexfo  5454  isocnv  5479  isoini  5485  isoselem  5487  riota2df  5516  ovmpt2dxf  5654  caovcanrd  5692  ordiso2  6415  ltpiord  6475  dfplpq2  6510  dfmpq2  6511  enqeceq  6515  enq0eceq  6593  enreceq  6879  cnegexlem3  7251  subeq0  7300  negcon1  7326  subexsub  7442  subeqrev  7446  lesub  7510  ltsub13  7512  subge0  7544  div11ap  7751  divmuleqap  7768  ltmuldiv2  7916  lemuldiv2  7923  nn1suc  8009  addltmul  8218  elnnnn0  8282  znn0sub  8367  prime  8396  indstr  8632  qapne  8671  qlttri2  8673  fz1n  9010  fzrev3  9051  fzonlt0  9125  divfl0  9246  modqsubdir  9343  fzfig  9370  sqrt11  9866  sqrtsq2  9870  absdiflt  9919  absdifle  9920  nnabscl  9927  clim2  10035  climshft2  10058  dvdscmulr  10136  dvdsmulcr  10137  oddm1even  10186  sqrt2irr  10251
 Copyright terms: Public domain W3C validator