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

Theorem biimp3ar 1472
Description: Infer implication from a logical equivalence. Similar to biimpar 481. (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 811 . 2 (𝜑 → (𝜓 → (𝜃𝜒)))
323imp 1113 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089
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 210  df-an 400  df-3an 1091
This theorem is referenced by:  rmoi  3803  brelrng  5810  fpr3g  8026  frrlem4  8030  dif1enlem  8838  div2sub  11657  nn0p1elfzo  13285  ssfzo12  13335  modltm1p1mod  13496  hashgt23el  13991  repswpfx  14350  abssubge0  14891  qredeu  16215  abvne0  19863  slesolinvbi  21578  basgen2  21886  fcfval  22930  nmne0  23517  ovolfsf  24368  logbprmirr  25679  lgssq  26218  lgssq2  26219  colinearalg  27001  usgr0v  27329  frgr0vb  28346  nv1  28756  adjeq  30016  pridln1  31332  revpfxsfxrev  32790  areacirc  35607  fvopabf4g  35616  exidreslem  35772  hgmapvvlem3  39676  iocmbl  40747  iunconnlem2  42228  ssfz12  44479  m1modmmod  45540
  Copyright terms: Public domain W3C validator