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

Theorem bitr3d 189
Description: Deduction form of bitr3i 185. (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 140 . 2 (𝜑 → (𝜒𝜓))
3 bitr3d.2 . 2 (𝜑 → (𝜓𝜃))
42, 3bitrd 187 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3bitrrd  214  3bitr3d  217  3bitr3rd  218  pm5.16  813  biassdc  1373  pm5.24dc  1376  anxordi  1378  sbequ12a  1746  drex1  1770  sbcomxyyz  1945  sb9v  1953  csbiebt  3039  prsspwg  3679  bnd2  4097  copsex2t  4167  copsex2g  4168  fnssresb  5235  fcnvres  5306  dmfco  5489  funimass5  5537  fmptco  5586  cbvfo  5686  cbvexfo  5687  isocnv  5712  isoini  5719  isoselem  5721  riota2df  5750  ovmpodxf  5896  caovcanrd  5934  fidcenumlemrks  6841  ordiso2  6920  ltpiord  7139  dfplpq2  7174  dfmpq2  7175  enqeceq  7179  enq0eceq  7257  enreceq  7556  ltpsrprg  7623  mappsrprg  7624  cnegexlem3  7951  subeq0  8000  negcon1  8026  subexsub  8146  subeqrev  8150  lesub  8215  ltsub13  8217  subge0  8249  div11ap  8472  divmuleqap  8489  ltmuldiv2  8645  lemuldiv2  8652  nn1suc  8751  addltmul  8968  elnnnn0  9032  znn0sub  9131  prime  9162  indstr  9400  qapne  9443  qlttri2  9445  fz1n  9836  fzrev3  9879  fzonlt0  9956  divfl0  10081  modqsubdir  10178  fzfig  10215  sqrt11  10823  sqrtsq2  10827  absdiflt  10876  absdifle  10877  nnabscl  10884  minclpr  11020  xrnegiso  11043  xrnegcon1d  11045  clim2  11064  climshft2  11087  sumrbdc  11160  prodrbdclem2  11354  sinbnd  11470  cosbnd  11471  dvdscmulr  11533  dvdsmulcr  11534  oddm1even  11583  qredeq  11788  cncongr2  11796  isprm3  11810  prmrp  11834  sqrt2irr  11851  crth  11911  eltg3  12240  eltop  12252  eltop2  12253  eltop3  12254  lmbrf  12398  cncnpi  12411  txcn  12458  hmeoimaf1o  12497  ismet2  12537  xmseq0  12651
  Copyright terms: Public domain W3C validator