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

Theorem biimp3a 1469
Description: Infer implication from a logical equivalence. Similar to biimpa 477. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
biimp3a.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
biimp3a ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem biimp3a
StepHypRef Expression
1 biimp3a.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21biimpa 477 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1110 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  onomeneq  9168  nn0addge1  12455  nn0addge2  12456  nn0sub2  12560  eluzp1p1  12787  uznn0sub  12794  uzinfi  12845  iocssre  13336  icossre  13337  iccssre  13338  lincmb01cmp  13404  iccf1o  13405  fzosplitprm1  13674  subfzo0  13686  modfzo0difsn  13840  hashprb  14289  pfxpfx  14588  eflt  15991  fldivndvdslt  16288  prmdiv  16649  hashgcdlem  16652  vfermltl  16665  coprimeprodsq  16672  pythagtrip  16698  difsqpwdvds  16751  cshwshashlem2  16961  odinf  19336  odcl2  19338  slesolex  22015  tgtop11  22316  restntr  22517  hauscmplem  22741  icchmeo  24288  pi1xfr  24402  sinq12gt0  25848  tanord1  25877  gausslemma2dlem1a  26697  sltn0  27218  axsegconlem6  27757  lfuhgr1v0e  28088  crctcshwlkn0lem6  28646  crctcshwlkn0lem7  28647  clwlkclwwlkf1lem2  28835  s2elclwwlknon2  28934  eucrctshift  29073  eucrct2eupth  29075  nv1  29503  lnolin  29582  br8d  31415  fzm1ne1  31575  ismntd  31727  mntf  31728  cycpmco2lem6  31863  ballotlemfc0  32961  ballotlemfcc  32962  ballotlemrv2  32990  fisshasheq  33574  br8  34199  br6  34200  br4  34201  bj-imdiridlem  35623  ismtyima  36229  ismtybndlem  36232  ghomlinOLD  36314  ghomidOLD  36315  cvrcmp2  37713  atcvrj2  37863  1cvratex  37903  lplnric  37982  lplnri1  37983  lnatexN  38209  ltrnateq  38611  ltrnatneq  38612  cdleme46f2g2  38923  cdleme46f2g1  38924  dibelval1st  39579  dibelval2nd  39582  dicelval1sta  39617  hlhilphllem  40393  jm2.17b  41223  bi123impia  42713  sineq0ALT  43161  eliccre  43675  ioomidp  43684  smfinflem  44990  iccpartiltu  45546  goldbachthlem1  45669  evengpop3  45922  rnghmresel  46194  rhmresel  46240  itcovalsuc  46685
  Copyright terms: Public domain W3C validator