MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imp2 Unicode version

Theorem 3imp2 1211
Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3imp1.1
Assertion
Ref Expression
3imp2

Proof of Theorem 3imp2
StepHypRef Expression
1 3imp1.1 . . 3
213impd 1210 . 2
32imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  wereu  4880  ovg  6441  fisup2g  7947  cfcoflem  8673  ttukeylem5  8914  dedekindle  9766  grplcan  16102  mulgnnass  16170  dmdprdsplit2  17095  mulgass2  17247  lmodvsdi  17535  lmodvsdir  17536  lmodvsass  17537  lss1d  17609  islmhm2  17684  lspsolvlem  17788  lbsextlem2  17805  cygznlem2a  18606  isphld  18689  t0dist  19826  hausnei  19829  nrmsep3  19856  fclsopni  20516  fcfneii  20538  ax5seglem5  24236  axcont  24279  grporcan  25223  grpolcan  25235  ghgrpOLD  25370  slmdvsdi  27758  slmdvsdir  27759  slmdvsass  27760  mclsppslem  28943  broutsideof2  29772  frinfm  30226  crngm23  30399  pridl  30434  pridlc  30468  dmnnzd  30472  dmncan1  30473  paddasslem5  35548
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator