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

Theorem biimp3ar 1425
Description: Infer implication from a logical equivalence. Similar to biimpar 501. (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 650 . 2 (𝜑 → (𝜓 → (𝜃𝜒)))
323imp 1249 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  rmoi  3496  brelrng  5276  div2sub  10729  nn0p1elfzo  12378  ssfzo12  12427  modltm1p1mod  12584  abssubge0  13915  qredeu  15210  abvne0  18650  slesolinvbi  20306  basgen2  20604  fcfval  21647  nmne0  22233  ovolfsf  23047  lgssq  24862  lgssq2  24863  colinearalg  25590  nv1  26914  adjeq  28178  areacirc  32675  fvopabf4g  32685  exidreslem  32846  hgmapvvlem3  36235  iocmbl  36817  iunconlem2  38193  ssfz12  40351  usgr0v  40467  frgr0vb  41434  m1modmmod  42110
  Copyright terms: Public domain W3C validator