MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr2id Structured version   Visualization version   GIF version

Theorem bitr2id 284
Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.)
Hypotheses
Ref Expression
bitr2id.1 (𝜑𝜓)
bitr2id.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
bitr2id (𝜒 → (𝜃𝜑))

Proof of Theorem bitr2id
StepHypRef Expression
1 bitr2id.1 . . 3 (𝜑𝜓)
2 bitr2id.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2bitrid 283 . 2 (𝜒 → (𝜑𝜃))
43bicomd 223 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 207
This theorem is referenced by:  bitr3di  286  necon1abid  2979  necon4abid  2981  uniiunlem  4087  r19.9rzv  4500  2reu4lem  4522  intprg  4981  inimasn  6176  fnresdisj  6688  fnsnfv  6988  f1oiso  7371  reldm  8069  rdglim2  8472  mptelixpg  8975  1idpr  11069  nndiv  12312  fz1sbc  13640  grpid  18993  isrnghm  20441  rnghmval2  20444  znleval  21573  fbunfip  23877  lmflf  24013  metcld2  25341  lgsne0  27379  isuvtx  29412  loopclwwlkn1b  30061  clwwlknun  30131  frgrncvvdeqlem2  30319  isph  30841  ofpreima  32675  fdifsupp  32694  ressply1mon1p  33593  eulerpartlemd  34368  bnj168  34744  cardpred  35104  opelco3  35775  wl-2sb6d  37559  poimirlem26  37653  cnambfre  37675  heibor1  37817  opltn0  39191  cvrnbtwn2  39276  cvrnbtwn4  39280  atlltn0  39307  pmapjat1  39855  dih1dimatlem  41331  2rexfrabdioph  42807  dnwech  43060  rfovcnvf1od  44017  uneqsn  44038  lighneallem2  47593  stgredgiun  47925
  Copyright terms: Public domain W3C validator