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

Theorem biimp3ar 1587
Description: Infer implication from a logical equivalence. Similar to biimpar 465. (Contributed by NM, 2-Jan-2009.)
Hypothesis
Ref Expression
biimp3a.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
biimp3ar ((𝜑𝜓𝜃) → 𝜒)

Proof of Theorem biimp3ar
StepHypRef Expression
1 biimp3a.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21exbiri 836 . 2 (𝜑 → (𝜓 → (𝜃𝜒)))
323imp 1130 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  rmoi  3725  brelrng  5556  div2sub  11135  nn0p1elfzo  12735  ssfzo12  12785  modltm1p1mod  12946  abssubge0  14290  qredeu  15590  abvne0  19031  slesolinvbi  20699  basgen2  21007  fcfval  22050  nmne0  22636  ovolfsf  23452  lgssq  25276  lgssq2  25277  colinearalg  26004  usgr0v  26349  frgr0vb  27437  nv1  27858  adjeq  29122  frrlem4  32104  areacirc  33817  fvopabf4g  33827  exidreslem  33987  hgmapvvlem3  37706  iocmbl  38298  iunconnlem2  39665  ssfz12  41899  m1modmmod  42884
  Copyright terms: Public domain W3C validator