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

Theorem biimp3ar 1471
Description: Infer implication from a logical equivalence. Similar to biimpar 479. (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 810 . 2 (𝜑 → (𝜓 → (𝜃𝜒)))
323imp 1112 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  rmoi  3885  brelrng  5939  fpr3g  8267  frrlem4  8271  dif1enlem  9153  dif1enlemOLD  9154  php3  9209  div2sub  12036  nn0p1elfzo  13672  ssfzo12  13722  modltm1p1mod  13885  hashgt23el  14381  repswpfx  14732  abssubge0  15271  qredeu  16592  abvne0  20428  slesolinvbi  22175  basgen2  22484  fcfval  23529  nmne0  24120  ovolfsf  24980  logbprmirr  26291  lgssq  26830  lgssq2  26831  colinearalg  28158  usgr0v  28488  frgr0vb  29506  nv1  29916  adjeq  31176  pridln1  32550  revpfxsfxrev  34095  areacirc  36570  fvopabf4g  36579  exidreslem  36734  hgmapvvlem3  40785  iocmbl  41948  iunconnlem2  43682  ssfz12  46009  m1modmmod  47161
  Copyright terms: Public domain W3C validator